awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin x).radius) y
x_add_y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) (x + y)
f : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l } → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
hsf : Summable f
hf : HasSum f ((p.changeOrigin x).sum y)
⊢ HasSum (β := (n : ℕ) × Finset (Fin n))
    (f ∘
      (⇑changeOriginIndexEquiv.symm :
        (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
    (p.sum (x + y))
have refine : ∀ (n : ℕ),
  HasSum.{u_3, 0} (α := F)
    (fun (c : Finset (Fin n)) ↦
      Function.comp (α := (n : ℕ) × Finset (Fin n)) f
        (⇑changeOriginIndexEquiv.symm :
          (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
        (Sigma.mk (β := fun (b : ℕ) ↦ Finset (Fin b)) n c))
    ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ x + y : F)
Tactic: refine HasSum.sigma_of_hasSum
    (p.hasSum x_add_y_mem_ball) (fun n => ?_) (changeOriginIndexEquiv.symm.summable_iff.2 hsf)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
⊢ r - ‖y‖ₑ ≤ (p.changeOrigin y).radius
have apply : r - ‖y‖ₑ ≤ p.radius - (↑‖y‖₊ : ℝ≥0∞)
Tactic: apply le_trans _ p.changeOrigin_radius
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
⊢ f (x + y + z) = (p.changeOrigin y).sum z
have hz₁ : ‖y‖ₑ + ‖z‖ₑ < r
Tactic: rw [mem_eball_zero_iff, lt_tsub_iff_right, add_comm] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
⊢ f (x + y + z) = (p.changeOrigin y).sum z
have h'y : x + (y + z) ∈ insert x s
Tactic: rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
h'y : x + (y + z) ∈ insert x s
⊢ f (x + y + z) = (p.changeOrigin y).sum z
have hy₁ : Membership.mem (γ := Set E) (Metric.eball 0 r) (y + z)
Tactic: rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
⊢ x + (y + z) ∈ insert x s
have this : insert (x + y) s ⊆ insert (x + y) (insert x s)
Tactic: have : insert (x + y) s ⊆ insert (x + y) (insert x s) := by
          apply insert_subset_insert (subset_insert _ _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
this : insert (x + y) s ⊆ insert (x + y) (insert x s)
⊢ x + (y + z) ∈ insert x s
have this₁ : insert (x + y) s ⊆ insert x s
Tactic: rw [insert_eq_of_mem hy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
this : insert (x + y) s ⊆ insert x s
⊢ x + (y + z) ∈ insert x s
have h'y : x + (y + z) ∈ insert (x + y) s
Tactic: apply this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
⊢ HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + y + z))
have this : f (x + y + z) = (p.changeOrigin y).sum z
Tactic: have : f (x + y + z) =
        FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by
      rw [mem_eball_zero_iff, lt_tsub_iff_right, add_comm] at hz
      rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum]
      · have : insert (x + y) s ⊆ insert (x + y) (insert x s) := by
          apply insert_subset_insert (subset_insert _ _)
        rw [insert_eq_of_mem hy] at this
        apply this
        simpa [add_assoc] using h'z
      exact mem_eball_zero_iff.2 (lt_of_le_of_lt (enorm_add_le _ _) hz)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
this : f (x + y + z) = (p.changeOrigin y).sum z
⊢ HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + y + z))
have rw : HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) ((p.changeOrigin y).sum z)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
this : f (x + y + z) = (p.changeOrigin y).sum z
⊢ HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) ((p.changeOrigin y).sum z)
have apply : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin y).radius) z
Tactic: apply (p.changeOrigin y).hasSum
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - ‖y‖ₑ)) z
this : f (x + y + z) = (p.changeOrigin y).sum z
⊢ Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin y).radius) z
have refine : r - ‖y‖ₑ ≤ p.radius - (↑‖y‖₊ : ℝ≥0∞)
Tactic: refine Metric.eball_subset_eball (le_trans ?_ p.changeOrigin_radius) hz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : (↑‖y‖₊ : ℝ≥0∞) < r
⊢ HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - (↑‖y‖₊ : ℝ≥0∞))
have rw : ∀ (hf : HasFPowerSeriesWithinOnBall f p univ x r) (h : (↑‖y‖₊ : ℝ≥0∞) < r),
  HasFPowerSeriesWithinOnBall f (p.changeOrigin y) univ (x + y) (r - (↑‖y‖₊ : ℝ≥0∞))
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
⊢ AnalyticWithinAt 𝕜 f s y
have this : (↑‖y - x‖₊ : ℝ≥0∞) < r
Tactic: have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using h.2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
this : (↑‖y - x‖₊ : ℝ≥0∞) < r
⊢ AnalyticWithinAt 𝕜 f s y
have this₁ : HasFPowerSeriesWithinOnBall f (p.changeOrigin (y - x)) s (x + (y - x)) (r - ‖y - x‖ₑ)
Tactic: have := hf.changeOrigin this (by simpa using h.1)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
this_1 : (↑‖y - x‖₊ : ℝ≥0∞) < r
this : HasFPowerSeriesWithinOnBall f (p.changeOrigin (y - x)) s (x + (y - x)) (r - ‖y - x‖ₑ)
⊢ AnalyticWithinAt 𝕜 f s y
have this₁ : HasFPowerSeriesWithinOnBall f (p.changeOrigin (y - x)) s y (r - ‖y - x‖ₑ)
Tactic: rw [add_sub_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : y ∈ Metric.eball x r
⊢ AnalyticAt 𝕜 f y
have hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ Metric.eball x r
⊢ AnalyticAt 𝕜 f y
have rw : AnalyticWithinAt 𝕜 f univ y
Tactic: rw [← analyticWithinAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : E | AnalyticAt 𝕜 f x}
have rw : ∀ (x : E), Membership.mem (γ := Set E) {x : E | AnalyticAt 𝕜 f x} x → {x : E | AnalyticAt 𝕜 f x} ∈ 𝓝 x
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
⊢ AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)
have pos : ∀ (hr : p.radius = 0), AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)
Tactic: by_cases hr : p.radius = 0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
pos : ∀ (hr : p.radius = 0), AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)
⊢ AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)
have neg : ∀ (hr : ¬p.radius = 0), AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)
Tactic: by_cases hr : p.radius = 0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ p.applyComposition (Composition.ones n) = fun (v : Fin n → E) (i : Fin (Composition.ones n).length) ↦
    (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ i)
have h : ∀ (v : Fin n → E) (i : Fin (Composition.ones n).length),
  p.applyComposition (Composition.ones n) v i = (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE sorry i)
Tactic: funext v i
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
i : Fin (Composition.ones n).length
⊢ p.applyComposition (Composition.ones n) v i = (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ i)
have h : ∀ (i_1 : ℕ) (him : i_1 < (Composition.ones n).blocksFun i) (hin : i_1 < 1),
  (v ∘ (⇑((Composition.ones n).embedding i) : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n))
      (⟨i_1, him⟩ : Fin ((Composition.ones n).blocksFun i)) =
    v (Fin.castLE sorry i)
Tactic: apply p.congr (Composition.ones_blocksFun _ _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
i : Fin (Composition.ones n).length
j : ℕ
hjn : j < (Composition.ones n).blocksFun i
hj1 : j < 1
⊢ (v ∘ (⇑((Composition.ones n).embedding i) : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n))
      (⟨j, hjn⟩ : Fin ((Composition.ones n).blocksFun i)) =
    v (Fin.castLE ⋯ i)
have h : ∀ (hjn : 0 < (Composition.ones n).blocksFun i) (hj1 : LT.lt (α := ℕ) 0 1),
  (v ∘ (⇑((Composition.ones n).embedding i) : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n))
      (⟨0, hjn⟩ : Fin ((Composition.ones n).blocksFun i)) =
    v (Fin.castLE sorry i)
Tactic: obtain rfl : j = 0 := by lia
Cleared hypotheses: j, hjn, hj1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
i : Fin (Composition.ones n).length
hjn : 0 < (Composition.ones n).blocksFun i
hj1 : LT.lt (α := ℕ) 0 1
⊢ (v ∘ (⇑((Composition.ones n).embedding i) : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n))
      (⟨0, hjn⟩ : Fin ((Composition.ones n).blocksFun i)) =
    v (Fin.castLE ⋯ i)
have h : ((Composition.ones n).embedding i : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n) ⟨0, hjn⟩ = Fin.castLE sorry i
Tactic: refine congr_arg v ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
i : Fin (Composition.ones n).length
hjn : 0 < (Composition.ones n).blocksFun i
hj1 : LT.lt (α := ℕ) 0 1
⊢ ((Composition.ones n).embedding i : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n) ⟨0, hjn⟩ = Fin.castLE ⋯ i
have h : (↑(((Composition.ones n).embedding i : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n)
        (⟨0, hjn⟩ : Fin ((Composition.ones n).blocksFun i))) :
    ℕ) =
  (↑(Fin.castLE sorry i) : ℕ)
Tactic: rw [Fin.ext_iff, Fin.val_castLE, Composition.ones_embedding, Fin.val_mk]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
i : Fin (Composition.ones n).length
hjn : 0 < (Composition.ones n).blocksFun i
hj1 : LT.lt (α := ℕ) 0 1
h :
  (↑(((Composition.ones n).embedding i : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n)
          (⟨0, hjn⟩ : Fin ((Composition.ones n).blocksFun i))) :
      ℕ) =
    (↑(Fin.castLE ⋯ i) : ℕ)
⊢ ((Composition.ones n).embedding i : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n) ⟨0, hjn⟩ = Fin.castLE ⋯ i
have h₁ : (↑(((Composition.ones n).embedding i : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n)
        (⟨0, hjn⟩ : Fin ((Composition.ones n).blocksFun i))) :
    ℕ) =
  (↑i : ℕ)
Tactic: rw [Fin.ext_iff, Fin.val_castLE, Composition.ones_embedding, Fin.val_mk]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
i : Fin (Composition.ones n).length
hjn : 0 < (Composition.ones n).blocksFun i
hj1 : LT.lt (α := ℕ) 0 1
h :
  (↑(((Composition.ones n).embedding i : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n)
          (⟨0, hjn⟩ : Fin ((Composition.ones n).blocksFun i))) :
      ℕ) =
    (↑(Fin.castLE ⋯ i) : ℕ)
h₁ :
  (↑(((Composition.ones n).embedding i : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n)
          (⟨0, hjn⟩ : Fin ((Composition.ones n).blocksFun i))) :
      ℕ) =
    (↑i : ℕ)
⊢ ((Composition.ones n).embedding i : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n) ⟨0, hjn⟩ = Fin.castLE ⋯ i
have h₂ : (↑(⟨(↑i : ℕ), sorry⟩ : Fin n) : ℕ) = (↑i : ℕ)
Tactic: rw [Fin.ext_iff, Fin.val_castLE, Composition.ones_embedding, Fin.val_mk]