awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
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
⊢ ({ 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

Tactic:
congr
-- Module: Mathlib.Analysis.Analytic.Composition
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
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)
⊢ Eq (α := FormalMultilinearSeries 𝕜 E H) (FormalMultilinearSeries.comp (r.comp q) p : FormalMultilinearSeries 𝕜 E H)
    (r.comp (q.comp p) : FormalMultilinearSeries 𝕜 E H)

Tactic:
ext n v
-- Module: Mathlib.Analysis.Analytic.Composition
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)))
this :
  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)
⊢ 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:
simpa +unfoldPartialApp only [FormalMultilinearSeries.comp,
      ContinuousMultilinearMap.sum_apply, compAlongComposition_apply, Finset.sum_sigma',
      applyComposition, ContinuousMultilinearMap.map_sum]

Premises used: ContinuousMultilinearMap.map_sum, ContinuousMultilinearMap.sum_apply, Finset.sum_sigma', FormalMultilinearSeries.applyComposition, FormalMultilinearSeries.compAlongComposition_apply, FormalMultilinearSeries.comp
-- Module: Mathlib.Analysis.Analytic.Composition
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)))
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)
⊢ 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:
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]
-- Module: Mathlib.Analysis.Analytic.Composition
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)))
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))
⊢ 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:
rw [← (sigmaEquivSigmaPi n).sum_comp]

Premises used: Equiv.sum_comp, Composition.sigmaEquivSigmaPi
-- Module: Mathlib.Analysis.Analytic.Composition
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)))
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)
⊢ 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:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Analytic.Composition
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_1 :
  Membership.mem (γ := Finset ((a : Composition n) × Composition a.length)) Finset.univ
    (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)
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))
⊢ 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))

Tactic:
dsimp [sigmaEquivSigmaPi]

Premises used: Composition.sigmaEquivSigmaPi
-- Module: Mathlib.Analysis.Analytic.Constructions
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
⊢ ∞ ≤ FormalMultilinearSeries.radius (constFormalMultilinearSeries 𝕜 E c)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Constructions
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
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)
⊢ HasFPowerSeriesOnBall (fun (x : E) ↦ c) (constFormalMultilinearSeries 𝕜 E c) e ∞

Tactic:
refine ⟨by simp, WithTop.top_pos, fun _ => hasSum_single 0 fun n hn => ?_⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
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 y : E
h : 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:
simp [constFormalMultilinearSeries_apply_of_nonzero hn]

Premises used: constFormalMultilinearSeries_apply_of_nonzero
-- Module: Mathlib.Analysis.Analytic.Constructions
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
⊢ HasFPowerSeriesAt (fun (x : E) ↦ c) (constFormalMultilinearSeries 𝕜 E c) e

Tactic:
⟨⊤, hasFPowerSeriesOnBall_const⟩

Premises used: hasFPowerSeriesOnBall_const, Exists.intro, HasFPowerSeriesAt, Top.top
-- Module: Mathlib.Analysis.Analytic.Constructions
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
v : F
x : E
⊢ AnalyticAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (x : E) ↦ v) x

Tactic:
⟨constFormalMultilinearSeries 𝕜 E v, hasFPowerSeriesAt_const⟩

Premises used: hasFPowerSeriesAt_const, constFormalMultilinearSeries, AnalyticAt, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Constructions
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
v : F
s : Set E
⊢ AnalyticOnNhd.{u_2, u_3, u_4} 𝕜 (F := F) (fun (x : E) ↦ v) s

Tactic:
fun _ _ => analyticAt_const

Premises used: AnalyticOnNhd, analyticAt_const
-- Module: Mathlib.Analysis.Analytic.Constructions
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
v : F
s : Set E
x : E
⊢ AnalyticWithinAt.{u_2, u_3, u_4} 𝕜 (F := F) (fun (x : E) ↦ v) s x

Tactic:
analyticAt_const.analyticWithinAt

Premises used: analyticAt_const, AnalyticAt.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.Constructions
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
v : F
s : Set E
⊢ AnalyticOn.{u_2, u_3, u_4} 𝕜 (F := F) (fun (x : E) ↦ v) s

Tactic:
analyticOnNhd_const.analyticOn

Premises used: analyticOnNhd_const, AnalyticOnNhd.analyticOn
-- Module: Mathlib.Analysis.Analytic.Constructions
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
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
hg : HasFPowerSeriesWithinOnBall g pg s x r
⊢ HasFPowerSeriesWithinOnBall (f + g) (pf + pg) s x r

Tactic:
{ r_le := le_trans (le_min_iff.2 ⟨hf.r_le, hg.r_le⟩) (pf.min_radius_le_radius_add pg)
    r_pos := hf.r_pos
    hasSum := fun hy h'y => (hf.hasSum hy h'y).add (hg.hasSum hy h'y) }

Premises used: Iff.mpr, HasSum.add, HasFPowerSeriesWithinOnBall.mk, HasFPowerSeriesWithinOnBall.r_le, And.intro, FormalMultilinearSeries.min_radius_le_radius_add, HasFPowerSeriesWithinOnBall.r_pos, HasFPowerSeriesWithinOnBall.hasSum, le_min_iff, le_trans
-- Module: Mathlib.Analysis.Analytic.Constructions
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
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
hg : HasFPowerSeriesOnBall g pg x r
⊢ HasFPowerSeriesOnBall (f + g) (pf + pg) x r

Tactic:
{ r_le := le_trans (le_min_iff.2 ⟨hf.r_le, hg.r_le⟩) (pf.min_radius_le_radius_add pg)
    r_pos := hf.r_pos
    hasSum := fun hy => (hf.hasSum hy).add (hg.hasSum hy) }

Premises used: Iff.mpr, HasSum.add, HasFPowerSeriesOnBall.r_le, HasFPowerSeriesOnBall.hasSum, HasFPowerSeriesOnBall.mk, And.intro, FormalMultilinearSeries.min_radius_le_radius_add, le_min_iff, HasFPowerSeriesOnBall.r_pos, le_trans
-- Module: Mathlib.Analysis.Analytic.Constructions
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
rcases :
  ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesWithinOnBall f pf s x r ∧ HasFPowerSeriesWithinOnBall g pg s x r),
    HasFPowerSeriesWithinAt (f + g) (pf + pg) s x
⊢ HasFPowerSeriesWithinAt (f + g) (pf + pg) s x

Tactic:
rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩

Premises used: HasFPowerSeriesWithinAt.eventually, Filter.Eventually.and, Filter.Eventually.exists
-- Module: Mathlib.Analysis.Analytic.Constructions
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
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f pf s x r ∧ HasFPowerSeriesWithinOnBall g pg s x r
⊢ HasFPowerSeriesWithinAt (f + g) (pf + pg) s x

Tactic:
⟨r, hr.1.add hr.2⟩

Premises used: And.right, And.left, HasFPowerSeriesWithinAt, Exists.intro, HasFPowerSeriesWithinOnBall.add
-- Module: Mathlib.Analysis.Analytic.Constructions
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
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f pf s x r ∧ HasFPowerSeriesWithinOnBall g pg s x r
⊢ HasFPowerSeriesWithinAt (f + g) (pf + pg) s x

Tactic:
exact ⟨r, hr.1.add hr.2⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
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
rcases :
  ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesOnBall f pf x r ∧ HasFPowerSeriesOnBall g pg x r),
    HasFPowerSeriesAt (f + g) (pf + pg) x
⊢ HasFPowerSeriesAt (f + g) (pf + pg) x

Tactic:
rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩

Premises used: Filter.Eventually.and, HasFPowerSeriesAt.eventually, Filter.Eventually.exists
-- Module: Mathlib.Analysis.Analytic.Constructions
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
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f pf x r ∧ HasFPowerSeriesOnBall g pg x r
⊢ HasFPowerSeriesAt (f + g) (pf + pg) x

Tactic:
⟨r, hr.1.add hr.2⟩

Premises used: HasFPowerSeriesOnBall.add, And.right, And.left, Exists.intro, HasFPowerSeriesAt
-- Module: Mathlib.Analysis.Analytic.Constructions
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
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f pf x r ∧ HasFPowerSeriesOnBall g pg x r
⊢ HasFPowerSeriesAt (f + g) (pf + pg) x

Tactic:
exact ⟨r, hr.1.add hr.2⟩