awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
n_1 n : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn (n := c.length) fun (i : Fin c.length) ↦ (d i).blocks) = c.blocks
e_2 :
  ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯, blocks_sum := ⋯ :
            Composition n }.gather
        ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } :
          Composition
            { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                blocks_sum := ⋯ : Composition n }.length)).length =
    c.length
i :
  Fin
    ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
            blocks_sum := ⋯ : Composition n }.gather
        ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } :
          Composition
            { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                blocks_sum := ⋯ : Composition n }.length)).length
⊢ getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length)
      (splitWrtComposition (n :=
        { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
            blocks_sum := ⋯ : Composition n }.length)
        (flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks))
        ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } :
          Composition
            { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                blocks_sum := ⋯ : Composition n }.length))
      (↑i : ℕ) ⋯ =
    blocks (n := c.blocksFun ⟨(↑i : ℕ), ⋯⟩) (d ⟨(↑i : ℕ), ⋯⟩)
have h : getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length)
    (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks) (↑i : ℕ) sorry =
  blocks (n := c.blocksFun ⟨(↑i : ℕ), sorry⟩) (d ⟨(↑i : ℕ), sorry⟩)
Tactic: rw [getElem_of_eq (splitWrtComposition_flatten _ _ _)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
n_1 n : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn (n := c.length) fun (i : Fin c.length) ↦ (d i).blocks) = c.blocks
e_2 :
  ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯, blocks_sum := ⋯ :
            Composition n }.gather
        ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } :
          Composition
            { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                blocks_sum := ⋯ : Composition n }.length)).length =
    c.length
i :
  Fin
    ({ blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
            blocks_sum := ⋯ : Composition n }.gather
        ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } :
          Composition
            { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                blocks_sum := ⋯ : Composition n }.length)).length
h :
  getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length)
      (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks) (↑i : ℕ) ⋯ =
    blocks (n := c.blocksFun ⟨(↑i : ℕ), ⋯⟩) (d ⟨(↑i : ℕ), ⋯⟩)
⊢ getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length)
      (splitWrtComposition (n :=
        { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
            blocks_sum := ⋯ : Composition n }.length)
        (flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks))
        ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } :
          Composition
            { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := ⋯,
                blocks_sum := ⋯ : Composition n }.length))
      (↑i : ℕ) ⋯ =
    blocks (n := c.blocksFun ⟨(↑i : ℕ), ⋯⟩) (d ⟨(↑i : ℕ), ⋯⟩)
have rw : List.map (α := List ℕ) List.length (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks) =
  blocks (n := List.length (α := ℕ) (flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks)))
    ({ blocks := ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).length, blocks_pos := sorry, blocks_sum := sorry } :
      Composition
        { blocks := flatten (ofFn (n := c.length) fun (j : Fin c.length) ↦ (d j).blocks), blocks_pos := sorry,
            blocks_sum := sorry : Composition n }.length)
Tactic: rw [getElem_of_eq (splitWrtComposition_flatten _ _ _)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
⊢ Eq (α := FormalMultilinearSeries 𝕜 E H) (FormalMultilinearSeries.comp (r.comp q) p : FormalMultilinearSeries 𝕜 E H)
    (r.comp (q.comp p) : FormalMultilinearSeries 𝕜 E H)
have h : ∀ (n : ℕ) (v : (i : Fin n) → E),
  Eq.{u_5 + 1} (α := H) ((FormalMultilinearSeries.comp (r.comp q) p n : (a : (i : Fin n) → E) → H) v : H)
    ((r.comp (q.comp p) n : (a : (i : Fin n) → E) → H) v : H)
Tactic: ext n v
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : (i : Fin n) → E
f : (a : Composition n) × Composition a.length → H :=
  fun (c : (a : Composition n) × Composition a.length) ↦
    (r c.snd (β := fun (a : Composition n) ↦ Composition a.length).length : (a : (i : Fin c.snd.length) → G) → H)
      (q.applyComposition (c.snd (β := fun (a : Composition n) ↦ Composition a.length))
        (p.applyComposition (c.fst (β := fun (a : Composition n) ↦ Composition a.length)) v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun (c : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) ↦
    (r c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length :
        (a : (i : Fin c.fst.length) → G) → H)
      fun (i : Fin c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (q (c.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).length :
          (a : (i : Fin (c.snd i).length) → F) → G)
        (p.applyComposition (c.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i)
          (v ∘
            (⇑(c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).embedding i) :
              (a : Fin (c.fst.blocksFun i)) → Fin n)))
⊢ Eq.{u_5 + 1} (α := H) ((FormalMultilinearSeries.comp (r.comp q) p n : (a : (i : Fin n) → E) → H) v : H)
    ((r.comp (q.comp p) n : (a : (i : Fin n) → E) → H) v : H)
have h : Eq.{u_5 + 1} (α := H) (∑ c : (a : Composition n) × Composition a.length, f c)
  (∑ c : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)), g c)
Tactic: suffices ∑ c, f c = ∑ c, g c by
    simpa +unfoldPartialApp only [FormalMultilinearSeries.comp,
      ContinuousMultilinearMap.sum_apply, compAlongComposition_apply, Finset.sum_sigma',
      applyComposition, ContinuousMultilinearMap.map_sum]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : (i : Fin n) → E
f : (a : Composition n) × Composition a.length → H :=
  fun (c : (a : Composition n) × Composition a.length) ↦
    (r c.snd (β := fun (a : Composition n) ↦ Composition a.length).length : (a : (i : Fin c.snd.length) → G) → H)
      (q.applyComposition (c.snd (β := fun (a : Composition n) ↦ Composition a.length))
        (p.applyComposition (c.fst (β := fun (a : Composition n) ↦ Composition a.length)) v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun (c : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) ↦
    (r c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length :
        (a : (i : Fin c.fst.length) → G) → H)
      fun (i : Fin c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (q (c.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).length :
          (a : (i : Fin (c.snd i).length) → F) → G)
        (p.applyComposition (c.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i)
          (v ∘
            (⇑(c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).embedding i) :
              (a : Fin (c.fst.blocksFun i)) → Fin n)))
⊢ Eq.{u_5 + 1} (α := H) (∑ c : (a : Composition n) × Composition a.length, f c)
    (∑ c : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)), g c)
have h : Eq.{u_5 + 1} (α := H) (∑ c : (a : Composition n) × Composition a.length, f c)
  (∑ i : (a : Composition n) × Composition a.length,
    g
      ((sigmaEquivSigmaPi n :
          (a : (a : Composition n) × Composition a.length) →
            (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)))
        i))
Tactic: rw [← (sigmaEquivSigmaPi n).sum_comp]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : (i : Fin n) → E
f : (a : Composition n) × Composition a.length → H :=
  fun (c : (a : Composition n) × Composition a.length) ↦
    (r c.snd (β := fun (a : Composition n) ↦ Composition a.length).length : (a : (i : Fin c.snd.length) → G) → H)
      (q.applyComposition (c.snd (β := fun (a : Composition n) ↦ Composition a.length))
        (p.applyComposition (c.fst (β := fun (a : Composition n) ↦ Composition a.length)) v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun (c : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) ↦
    (r c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length :
        (a : (i : Fin c.fst.length) → G) → H)
      fun (i : Fin c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (q (c.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).length :
          (a : (i : Fin (c.snd i).length) → F) → G)
        (p.applyComposition (c.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i)
          (v ∘
            (⇑(c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).embedding i) :
              (a : Fin (c.fst.blocksFun i)) → Fin n)))
⊢ Eq.{u_5 + 1} (α := H) (∑ c : (a : Composition n) × Composition a.length, f c)
    (∑ i : (a : Composition n) × Composition a.length,
      g
        ((sigmaEquivSigmaPi n :
            (a : (a : Composition n) × Composition a.length) →
              (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)))
          i))
have h : ∀ (x : (a : Composition n) × Composition a.length),
  Membership.mem (γ := Finset ((a : Composition n) × Composition a.length)) Finset.univ x →
    f x =
      g
        ((sigmaEquivSigmaPi n :
            (a : (a : Composition n) × Composition a.length) →
              (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)))
          x)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : (i : Fin n) → E
f : (a : Composition n) × Composition a.length → H :=
  fun (c : (a : Composition n) × Composition a.length) ↦
    (r c.snd (β := fun (a : Composition n) ↦ Composition a.length).length : (a : (i : Fin c.snd.length) → G) → H)
      (q.applyComposition (c.snd (β := fun (a : Composition n) ↦ Composition a.length))
        (p.applyComposition (c.fst (β := fun (a : Composition n) ↦ Composition a.length)) v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun (c : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) ↦
    (r c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length :
        (a : (i : Fin c.fst.length) → G) → H)
      fun (i : Fin c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (q (c.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).length :
          (a : (i : Fin (c.snd i).length) → F) → G)
        (p.applyComposition (c.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i)
          (v ∘
            (⇑(c.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).embedding i) :
              (a : Fin (c.fst.blocksFun i)) → Fin n)))
a : Composition n
b : Composition a.length
h :
  Membership.mem (γ := Finset ((a : Composition n) × Composition a.length)) Finset.univ
    (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)
⊢ f (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b) =
    g
      ((sigmaEquivSigmaPi n :
          (a : (a : Composition n) × Composition a.length) →
            (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)))
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b))
have h : f (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b) =
  g
    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) (a.gather b)
      (a.sigmaCompositionAux b))
Tactic: dsimp [sigmaEquivSigmaPi]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
c : F
e : E
⊢ HasFPowerSeriesOnBall (fun (x : E) ↦ c) (constFormalMultilinearSeries 𝕜 E c) e ∞
have refine : ∀ {y : E},
  Membership.mem (γ := Set E) (Metric.eball 0 ∞) y →
    ∀ (n : ℕ) (hn : n ≠ 0),
      Eq.{u_4 + 1} (α := F) ((constFormalMultilinearSeries 𝕜 E c n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)
        (0 : F)
Tactic: refine ⟨by simp, WithTop.top_pos, fun _ => hasSum_single 0 fun n hn => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f pf s x
hg : HasFPowerSeriesWithinAt g pg s x
⊢ HasFPowerSeriesWithinAt (f + g) (pf + pg) s x
have rcases : ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesWithinOnBall f pf s x r ∧ HasFPowerSeriesWithinOnBall g pg s x r),
  HasFPowerSeriesWithinAt (f + g) (pf + pg) s x
Tactic: rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f pf x
hg : HasFPowerSeriesAt g pg x
⊢ HasFPowerSeriesAt (f + g) (pf + pg) x
have rcases : ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesOnBall f pf x r ∧ HasFPowerSeriesOnBall g pg x r),
  HasFPowerSeriesAt (f + g) (pf + pg) x
Tactic: rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ (-pf).radius
have rw : r ≤ pf.radius
Tactic: rw [pf.radius_neg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ (-pf).radius
have rw : r ≤ pf.radius
Tactic: rw [pf.radius_neg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
⊢ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G) = min p.radius q.radius
have a : (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G) ≤ min p.radius q.radius
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
a : (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G) ≤ min p.radius q.radius
⊢ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G) = min p.radius q.radius
have a₁ : min p.radius q.radius ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
⊢ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G) ≤ min p.radius q.radius
have a : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)), (↑r : ℝ≥0∞) ≤ min p.radius q.radius
Tactic: refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
⊢ (↑r : ℝ≥0∞) ≤ min p.radius q.radius
have a : (↑r : ℝ≥0∞) ≤ p.radius ∧ (↑r : ℝ≥0∞) ≤ q.radius
Tactic: rw [le_min_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
⊢ (↑r : ℝ≥0∞) ≤ p.radius ∧ (↑r : ℝ≥0∞) ≤ q.radius
have this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
Tactic: have := (p.prod q).isLittleO_one_of_lt_radius hr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
⊢ (↑r : ℝ≥0∞) ≤ p.radius ∧ (↑r : ℝ≥0∞) ≤ q.radius
have a : (↑r : ℝ≥0∞) ≤ p.radius
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
a : (↑r : ℝ≥0∞) ≤ p.radius
⊢ (↑r : ℝ≥0∞) ≤ p.radius ∧ (↑r : ℝ≥0∞) ≤ q.radius
have a₁ : (↑r : ℝ≥0∞) ≤ q.radius
Tactic: constructor