awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
n : ℕ
c : Composition n
⊢ norm.{u_4} (E := G)
      ((q.compAlongComposition p
              ((Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n)) :
            (a : (i : Fin ⟨n, c⟩.fst) → E) → G)
          fun (_j : Fin ((Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).fst (β := fun (n : ℕ) ↦ Composition n))) ↦
          y :
        G) ≤
    ‖q.compAlongComposition p
          ((Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n))‖ *
      (↑r1 : ℝ) ^ (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).fst (β := fun (n : ℕ) ↦ Composition n)
have q₁ : norm.{u_4} (E := G) ((q.compAlongComposition p c : (a : (i : Fin n) → E) → G) fun (_j : Fin n) ↦ y : G) ≤
  ‖q.compAlongComposition p c‖ * ∏ _j : Fin n, ‖y‖
Tactic: calc
        ‖(compAlongComposition q p c) fun _j : Fin n => y‖ ≤
            ‖compAlongComposition q p c‖ * ∏ _j : Fin n, ‖y‖ := by
          apply ContinuousMultilinearMap.le_opNorm
        _ ≤ ‖compAlongComposition q p c‖ * (r1 : ℝ) ^ n := by
          apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
          rw [Finset.prod_const, Finset.card_fin]
          gcongr
          rw [Metric.mem_eball, edist_zero_right] at hy
          have := le_trans (le_of_lt hy) (min_le_right _ _)
          rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
n : ℕ
c : Composition n
q₁ :
  norm.{u_4} (E := G) ((q.compAlongComposition p c : (a : (i : Fin n) → E) → G) fun (_j : Fin n) ↦ y : G) ≤
    ‖q.compAlongComposition p c‖ * ∏ _j : Fin n, ‖y‖
⊢ norm.{u_4} (E := G)
      ((q.compAlongComposition p
              ((Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n)) :
            (a : (i : Fin ⟨n, c⟩.fst) → E) → G)
          fun (_j : Fin ((Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).fst (β := fun (n : ℕ) ↦ Composition n))) ↦
          y :
        G) ≤
    ‖q.compAlongComposition p
          ((Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n))‖ *
      (↑r1 : ℝ) ^ (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).fst (β := fun (n : ℕ) ↦ Composition n)
have q₂ : ‖q.compAlongComposition p c‖ * ∏ _j : Fin n, ‖y‖ ≤ ‖q.compAlongComposition p c‖ * (↑r1 : ℝ) ^ n
Tactic: calc
        ‖(compAlongComposition q p c) fun _j : Fin n => y‖ ≤
            ‖compAlongComposition q p c‖ * ∏ _j : Fin n, ‖y‖ := by
          apply ContinuousMultilinearMap.le_opNorm
        _ ≤ ‖compAlongComposition q p c‖ * (r1 : ℝ) ^ n := by
          apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
          rw [Finset.prod_const, Finset.card_fin]
          gcongr
          rw [Metric.mem_eball, edist_zero_right] at hy
          have := le_trans (le_of_lt hy) (min_le_right _ _)
          rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
⊢ HasSum
    (fun (i : (n : ℕ) × Composition n) ↦
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    (f (x + y))
have cau : CauchySeq.{u_4, 0} (α := G) fun (s : Finset ((n : ℕ) × Composition n)) ↦
  ∑ i ∈ s,
    (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
      fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y
Tactic: have cau : CauchySeq fun s : Finset (Σ n, Composition n) =>
        ∑ i ∈ s, q.compAlongComposition p i.2 fun _j => y := by
      apply cauchySeq_finset_of_norm_bounded (NNReal.summable_coe.2 hr1) _
      simp only [coe_nnnorm, NNReal.coe_mul, NNReal.coe_pow]
      rintro ⟨n, c⟩
      calc
        ‖(compAlongComposition q p c) fun _j : Fin n => y‖ ≤
            ‖compAlongComposition q p c‖ * ∏ _j : Fin n, ‖y‖ := by
          apply ContinuousMultilinearMap.le_opNorm
        _ ≤ ‖compAlongComposition q p c‖ * (r1 : ℝ) ^ n := by
          apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
          rw [Finset.prod_const, Finset.card_fin]
          gcongr
          rw [Metric.mem_eball, edist_zero_right] at hy
          have := le_trans (le_of_lt hy) (min_le_right _ _)
          rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
cau :
  CauchySeq.{u_4, 0} (α := G) fun (s : Finset ((n : ℕ) × Composition n)) ↦
    ∑ i ∈ s,
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y
⊢ HasSum
    (fun (i : (n : ℕ) × Composition n) ↦
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    (f (x + y))
have apply : HasSum
  (fun (b : ℕ) ↦
    ∑ b_1 : Composition b,
      (q.compAlongComposition p
            ((Sigma.mk (β := fun (b : ℕ) ↦ Composition b) b b_1).snd (β := fun (n : ℕ) ↦ Composition n)) :
          (a : (i : Fin ⟨b, b_1⟩.fst) → E) → G)
        fun (_j : Fin ((Sigma.mk (β := fun (b : ℕ) ↦ Composition b) b b_1).fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
  (f (x + y))
Tactic: apply HasSum.of_sigma (fun b ↦ hasSum_fintype _) ?_ cau
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
⊢ Tendsto
    (fun (a : ℕ × ℕ) ↦
      q.partialSum a.1
        (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
    atTop (𝓝 (f (x + y)))
have A : HasSum
  (fun (i : (n : ℕ) × Composition n) ↦
    (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
      fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
  (f (x + y))
Tactic: have A : HasSum (fun i : Σ n, Composition n => q.compAlongComposition p i.2 fun _j => y)
      (f (x + y)) := by
    have cau : CauchySeq fun s : Finset (Σ n, Composition n) =>
        ∑ i ∈ s, q.compAlongComposition p i.2 fun _j => y := by
      apply cauchySeq_finset_of_norm_bounded (NNReal.summable_coe.2 hr1) _
      simp only [coe_nnnorm, NNReal.coe_mul, NNReal.coe_pow]
      rintro ⟨n, c⟩
      calc
        ‖(compAlongComposition q p c) fun _j : Fin n => y‖ ≤
            ‖compAlongComposition q p c‖ * ∏ _j : Fin n, ‖y‖ := by
          apply ContinuousMultilinearMap.le_opNorm
        _ ≤ ‖compAlongComposition q p c‖ * (r1 : ℝ) ^ n := by
          apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
          rw [Finset.prod_const, Finset.card_fin]
          gcongr
          rw [Metric.mem_eball, edist_zero_right] at hy
          have := le_trans (le_of_lt hy) (min_le_right _ _)
          rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
    apply HasSum.of_sigma (fun b ↦ hasSum_fintype _) ?_ cau
    simpa [FormalMultilinearSeries.comp] using h0.hasSum hy0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
A :
  HasSum
    (fun (i : (n : ℕ) × Composition n) ↦
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    (f (x + y))
⊢ Tendsto
    (fun (a : ℕ × ℕ) ↦
      q.partialSum a.1
        (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
    atTop (𝓝 (f (x + y)))
have B : Tendsto
  (fun (n : ℕ × ℕ) ↦
    ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
  atTop (𝓝 (f (x + y)))
Tactic: have B : Tendsto (fun (n : ℕ × ℕ) => ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
      q.compAlongComposition p i.2 fun _j => y) atTop (𝓝 (f (x + y))) := by
    apply Tendsto.comp A compPartialSumTarget_tendsto_prod_atTop
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
A :
  HasSum
    (fun (i : (n : ℕ) × Composition n) ↦
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    (f (x + y))
B :
  Tendsto
    (fun (n : ℕ × ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
        (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
          fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    atTop (𝓝 (f (x + y)))
⊢ Tendsto
    (fun (a : ℕ × ℕ) ↦
      q.partialSum a.1
        (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
    atTop (𝓝 (f (x + y)))
have C : Tendsto (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
  atTop (𝓝 (f (x + y)))
Tactic: have C : Tendsto (fun (n : ℕ × ℕ) => q.partialSum n.1 (∑ a ∈ Finset.Ico 1 n.2, p a fun _b ↦ y))
      atTop (𝓝 (f (x + y))) := by simpa [comp_partialSum] using B
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
A :
  HasSum
    (fun (i : (n : ℕ) × Composition n) ↦
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    (f (x + y))
B :
  Tendsto
    (fun (n : ℕ × ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
        (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
          fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    atTop (𝓝 (f (x + y)))
C :
  Tendsto (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (f (x + y)))
⊢ Tendsto
    (fun (a : ℕ × ℕ) ↦
      q.partialSum a.1
        (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
    atTop (𝓝 (f (x + y)))
have h : EventuallyEq.{0, u_4} (β := G) atTop
  (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
  fun (a : ℕ × ℕ) ↦
  q.partialSum a.1 (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F))
Tactic: apply C.congr'
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
A :
  HasSum
    (fun (i : (n : ℕ) × Composition n) ↦
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    (f (x + y))
B :
  Tendsto
    (fun (n : ℕ × ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
        (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
          fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    atTop (𝓝 (f (x + y)))
C :
  Tendsto (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (f (x + y)))
⊢ EventuallyEq.{0, u_4} (β := G) atTop
    (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    fun (a : ℕ × ℕ) ↦
    q.partialSum a.1
      (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F))
have h : ∀ (a : ℕ × ℕ),
  Membership.mem (γ := Set (ℕ × ℕ)) (Set.Ici (0, 1)) a →
    q.partialSum a.1 (∑ a ∈ Ico 1 a.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
      q.partialSum a.1
        (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F))
Tactic: filter_upwards [Ici_mem_atTop (0, 1)]
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
A :
  HasSum
    (fun (i : (n : ℕ) × Composition n) ↦
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    (f (x + y))
B :
  Tendsto
    (fun (n : ℕ × ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
        (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
          fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    atTop (𝓝 (f (x + y)))
C :
  Tendsto (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (f (x + y)))
fst n : ℕ
hn : 1 ≤ n
⊢ q.partialSum (fst, n).1 (∑ a ∈ Ico 1 (fst, n).2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    q.partialSum (fst, n).1
      (HSub.hSub (β := F) (p.partialSum (fst, n).2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F))
have h : (∑ a ∈ Ico 1 (fst, n).2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
  HSub.hSub (β := F) (p.partialSum (fst, n).2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)
Tactic: congr
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
A :
  HasSum
    (fun (i : (n : ℕ) × Composition n) ↦
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    (f (x + y))
B :
  Tendsto
    (fun (n : ℕ × ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
        (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
          fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    atTop (𝓝 (f (x + y)))
C :
  Tendsto (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (f (x + y)))
fst n : ℕ
hn : 1 ≤ n
⊢ (∑ a ∈ Ico 1 (fst, n).2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    HSub.hSub (β := F) (p.partialSum (fst, n).2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)
have h : HAdd.hAdd (α := F) (β := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)
    (∑ a ∈ Ico 1 (fst, n).2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y : F) =
  HAdd.hAdd (α := F) (β := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F)
    (∑ k ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) n, (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y : F)
Tactic: rw [partialSum, eq_sub_iff_add_eq', Finset.range_eq_Ico,
        Finset.sum_eq_sum_Ico_succ_bot hn]