awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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)
neg : ∀ (hr : ¬p.radius = 0), AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)
⊢ AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)

Tactic:
by_cases hr : p.radius = 0

Premises used: FormalMultilinearSeries.radius
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
hr : p.radius = 0
⊢ AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)

Tactic:
simp [hr]
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
hr : ¬p.radius = 0
⊢ AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)

Tactic:
(FormalMultilinearSeries.hasFPowerSeriesOnBall _ (pos_of_ne_zero hr)).analyticOnNhd

Premises used: HasFPowerSeriesOnBall.analyticOnNhd, pos_of_ne_zero, FormalMultilinearSeries.hasFPowerSeriesOnBall
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
hr : ¬p.radius = 0
⊢ AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)

Tactic:
exact (FormalMultilinearSeries.hasFPowerSeriesOnBall _ (pos_of_ne_zero hr)).analyticOnNhd

Premises used: HasFPowerSeriesOnBall.analyticOnNhd, pos_of_ne_zero, FormalMultilinearSeries.hasFPowerSeriesOnBall
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
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 ⋯ i)
⊢ 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)

Tactic:
funext v i
-- Module: Mathlib.Analysis.Analytic.Composition
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
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 ⋯ i)
⊢ p.applyComposition (Composition.ones n) v i = (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ i)

Tactic:
apply p.congr (Composition.ones_blocksFun _ _)

Premises used: FormalMultilinearSeries.congr, Composition.ones_blocksFun
-- Module: Mathlib.Analysis.Analytic.Composition
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
⊢ j = 0

Tactic:
lia
-- Module: Mathlib.Analysis.Analytic.Composition
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
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 ⋯ i)
⊢ (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)

Tactic:
obtain rfl : j = 0 := by lia

Premises used: rfl
-- Module: Mathlib.Analysis.Analytic.Composition
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)

Tactic:
congr_arg v ?_

Premises used: congr_arg
-- Module: Mathlib.Analysis.Analytic.Composition
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.castLE ⋯ i
⊢ (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)

Tactic:
refine congr_arg v ?_

Premises used: congr_arg
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ)
h₂ : (↑(⟨(↑i : ℕ), ⋯⟩ : Fin n) : ℕ) = (↑i : ℕ)
h₃ h₄ : (↑i : ℕ) = (↑i : ℕ)
⊢ ((Composition.ones n).embedding i : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n) ⟨0, hjn⟩ = Fin.castLE ⋯ i

Tactic:
rw [Fin.ext_iff, Fin.val_castLE, Composition.ones_embedding, Fin.val_mk]

Premises used: Fin.ext_iff, Fin.val_mk, Composition.ones_embedding, Fin.val_castLE
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
hn : 0 < n
v : Fin n → E
h :
  ∀ (j : Fin (Composition.single n hn).length),
    p.applyComposition (Composition.single n hn) v j = (p n : (a : (i : Fin n) → E) → F) v
⊢ p.applyComposition (Composition.single n hn) v = fun (_j : Fin (Composition.single n hn).length) ↦
    (p n : (a : (i : Fin n) → E) → F) v

Tactic:
ext j
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
hn : 0 < n
v : Fin n → E
j : Fin (Composition.single n hn).length
⊢ (Composition.single n hn).blocksFun j = n

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
hn : 0 < n
v : Fin n → E
j : Fin (Composition.single n hn).length
h :
  ∀ (i : ℕ) (hi1 : i < (Composition.single n hn).blocksFun j) (hi2 : i < n),
    (v ∘ (⇑((Composition.single n hn).embedding j) : (a : Fin ((Composition.single n hn).blocksFun j)) → Fin n))
        (⟨i, hi1⟩ : Fin ((Composition.single n hn).blocksFun j)) =
      v ⟨i, hi2⟩
⊢ p.applyComposition (Composition.single n hn) v j = (p n : (a : (i : Fin n) → E) → F) v

Tactic:
refine p.congr (by simp) fun i hi1 hi2 => ?_

Premises used: FormalMultilinearSeries.congr
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
hn : 0 < n
v : Fin n → E
j : Fin (Composition.single n hn).length
i : ℕ
hi1 : i < (Composition.single n hn).blocksFun j
hi2 : i < n
h :
  v
      (((Composition.single n hn).embedding j : (a : Fin ((Composition.single n hn).blocksFun j)) → Fin n)
        (⟨i, hi1⟩ : Fin ((Composition.single n hn).blocksFun j))) =
    v ⟨i, hi2⟩
⊢ (v ∘ (⇑((Composition.single n hn).embedding j) : (a : Fin ((Composition.single n hn).blocksFun j)) → Fin n))
      (⟨i, hi1⟩ : Fin ((Composition.single n hn).blocksFun j)) =
    v ⟨i, hi2⟩

Tactic:
dsimp
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
hn : 0 < n
v : Fin n → E
j : Fin (Composition.single n hn).length
i : ℕ
hi1 : i < (Composition.single n hn).blocksFun j
hi2 : i < n
h :
  ((Composition.single n hn).embedding j : (a : Fin ((Composition.single n hn).blocksFun j)) → Fin n) ⟨i, hi1⟩ =
    (⟨i, hi2⟩ : Fin n)
⊢ v
      (((Composition.single n hn).embedding j : (a : Fin ((Composition.single n hn).blocksFun j)) → Fin n)
        (⟨i, hi1⟩ : Fin ((Composition.single n hn).blocksFun j))) =
    v ⟨i, hi2⟩

Tactic:
congr 1
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
hn : 0 < n
v : Fin n → E
j : Fin (Composition.single n hn).length
i : ℕ
hi1 : i < (Composition.single n hn).blocksFun j
hi2 : i < n
⊢ ((Composition.single n hn).embedding 0 : (a : Fin ((Composition.single n hn).blocksFun 0)) → Fin n) ⟨i, hi2⟩ =
    (⟨i, hi2⟩ : Fin n)

Tactic:
Composition.single_embedding hn ⟨i, hi2⟩

Premises used: Fin.mk, Composition.single_embedding
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
hn : 0 < n
v : Fin n → E
j : Fin (Composition.single n hn).length
i : ℕ
hi1 : i < (Composition.single n hn).blocksFun j
hi2 : i < n
h :
  Eq (α := Fin n)
    (((Composition.single n hn).embedding j : (a : Fin ((Composition.single n hn).blocksFun j)) → Fin n) ⟨i, hi1⟩ :
      Fin n)
    (((Composition.single n hn).embedding 0 : (a : Fin ((Composition.single n hn).blocksFun 0)) → Fin n) ⟨i, hi2⟩ :
      Fin n)
⊢ ((Composition.single n hn).embedding j : (a : Fin ((Composition.single n hn).blocksFun j)) → Fin n) ⟨i, hi1⟩ =
    (⟨i, hi2⟩ : Fin n)

Tactic:
convert! Composition.single_embedding hn ⟨i, hi2⟩ using 1

Premises used: Fin.mk, Composition.single_embedding
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
hn : 0 < n
v : Fin n → E
j : Fin (Composition.single n hn).length
i : ℕ
hi1 : i < (Composition.single n hn).blocksFun j
hi2 : i < n
h :
  ∀ (j_val : ℕ) (j_property : j_val < (Composition.single n hn).length)
    (hi1 : i < (Composition.single n hn).blocksFun ⟨j_val, j_property⟩),
    Eq (α := Fin n)
      (((Composition.single n hn).embedding ⟨j_val, j_property⟩ :
            (a : Fin ((Composition.single n hn).blocksFun ⟨j_val, j_property⟩)) → Fin n)
          ⟨i, hi1⟩ :
        Fin n)
      (((Composition.single n hn).embedding 0 : (a : Fin ((Composition.single n hn).blocksFun 0)) → Fin n) ⟨i, hi2⟩ :
        Fin n)
⊢ Eq (α := Fin n)
    (((Composition.single n hn).embedding j : (a : Fin ((Composition.single n hn).blocksFun j)) → Fin n) ⟨i, hi1⟩ :
      Fin n)
    (((Composition.single n hn).embedding 0 : (a : Fin ((Composition.single n hn).blocksFun 0)) → Fin n) ⟨i, hi2⟩ :
      Fin n)

Tactic:
obtain ⟨j_val, j_property⟩ := j
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
hn : 0 < n
v : Fin n → E
i : ℕ
hi2 : i < n
j_val : ℕ
j_property : j_val < (Composition.single n hn).length
hi1 : i < (Composition.single n hn).blocksFun ⟨j_val, j_property⟩
⊢ j_val = 0

Tactic:
have : j_val = 0 := le_bot_iff.1 (Nat.lt_succ_iff.1 j_property)
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
hn : 0 < n
v : Fin n → E
i : ℕ
hi2 : i < n
j_val : ℕ
j_property : j_val < (Composition.single n hn).length
hi1 : i < (Composition.single n hn).blocksFun ⟨j_val, j_property⟩
this : j_val = 0
h :
  Eq (α := Fin n)
    (((Composition.single n hn).embedding ⟨0, ⋯⟩ : (a : Fin ((Composition.single n hn).blocksFun ⟨0, ⋯⟩)) → Fin n)
        ⟨i, ⋯⟩ :
      Fin n)
    (((Composition.single n hn).embedding 0 : (a : Fin ((Composition.single n hn).blocksFun 0)) → Fin n) ⟨i, hi2⟩ :
      Fin n)
⊢ Eq (α := Fin n)
    (((Composition.single n hn).embedding ⟨j_val, j_property⟩ :
          (a : Fin ((Composition.single n hn).blocksFun ⟨j_val, j_property⟩)) → Fin n)
        ⟨i, hi1⟩ :
      Fin n)
    (((Composition.single n hn).embedding 0 : (a : Fin ((Composition.single n hn).blocksFun 0)) → Fin n) ⟨i, hi2⟩ :
      Fin n)

Tactic:
rw! [this]
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
hn : 0 < n
v : Fin n → E
i : ℕ
hi2 : i < n
j_val : ℕ
j_property : j_val < (Composition.single n hn).length
hi1 : i < (Composition.single n hn).blocksFun ⟨j_val, j_property⟩
this : j_val = 0
⊢ Eq (α := Fin n)
    (((Composition.single n hn).embedding ⟨0, ⋯⟩ : (a : Fin ((Composition.single n hn).blocksFun ⟨0, ⋯⟩)) → Fin n)
        ⟨i, ⋯⟩ :
      Fin n)
    (((Composition.single n hn).embedding 0 : (a : Fin ((Composition.single n hn).blocksFun 0)) → Fin n) ⟨i, hi2⟩ :
      Fin n)

Tactic:
rfl
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
c : Composition n
h : ∀ (v : Fin n → E) (i : Fin c.length), p.removeZero.applyComposition c v i = p.applyComposition c v i
⊢ p.removeZero.applyComposition c = p.applyComposition c

Tactic:
ext v i
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
c : Composition n
v : Fin n → E
i : Fin c.length
⊢ p.removeZero.applyComposition c v i = p.applyComposition c v i

Tactic:
simp [applyComposition, zero_lt_one.trans_le (c.one_le_blocksFun i), removeZero_of_pos]

Premises used: FormalMultilinearSeries.removeZero_of_pos, FormalMultilinearSeries.applyComposition, zero_lt_one, LT.lt.trans_le, Composition.one_le_blocksFun
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
h :
  ∀ (k : Fin c.length),
    p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) k =
      Function.update (β := fun (a : Fin c.length) ↦ F) (p.applyComposition c v) (c.index j)
        ((p (c.blocksFun (c.index j)) : (a : (i : Fin (c.blocksFun (c.index j))) → E) → F)
          (Function.update (β := fun (i : Fin (c.blocksFun (c.index j))) ↦ E)
            (v ∘ (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)) (c.invEmbedding j) z))
        k
⊢ p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) =
    Function.update (β := fun (a : Fin c.length) ↦ F) (p.applyComposition c v) (c.index j)
      ((p (c.blocksFun (c.index j)) : (a : (i : Fin (c.blocksFun (c.index j))) → E) → F)
        (Function.update (β := fun (i : Fin (c.blocksFun (c.index j))) ↦ E)
          (v ∘ (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)) (c.invEmbedding j) z))

Tactic:
ext k
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
pos :
  ∀ (h : k = c.index j),
    p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) k =
      Function.update (β := fun (a : Fin c.length) ↦ F) (p.applyComposition c v) (c.index j)
        ((p (c.blocksFun (c.index j)) : (a : (i : Fin (c.blocksFun (c.index j))) → E) → F)
          (Function.update (β := fun (i : Fin (c.blocksFun (c.index j))) ↦ E)
            (v ∘ (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)) (c.invEmbedding j) z))
        k
neg :
  ∀ (h : ¬k = c.index j),
    p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) k =
      Function.update (β := fun (a : Fin c.length) ↦ F) (p.applyComposition c v) (c.index j)
        ((p (c.blocksFun (c.index j)) : (a : (i : Fin (c.blocksFun (c.index j))) → E) → F)
          (Function.update (β := fun (i : Fin (c.blocksFun (c.index j))) ↦ E)
            (v ∘ (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)) (c.invEmbedding j) z))
        k
⊢ p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) k =
    Function.update (β := fun (a : Fin c.length) ↦ F) (p.applyComposition c v) (c.index j)
      ((p (c.blocksFun (c.index j)) : (a : (i : Fin (c.blocksFun (c.index j))) → E) → F)
        (Function.update (β := fun (i : Fin (c.blocksFun (c.index j))) ↦ E)
          (v ∘ (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)) (c.invEmbedding j) z))
      k

Tactic:
by_cases h : k = c.index j

Premises used: Composition.index