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
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 : ℕ)
⊢ ((Composition.ones n).embedding i : (a : Fin ((Composition.ones n).blocksFun i)) → Fin n) ⟨0, hjn⟩ = Fin.castLE ⋯ i
have h₃ : (↑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 : ℕ
hn : 0 < n
v : Fin n → E
⊢ p.applyComposition (Composition.single n hn) v = fun (_j : Fin (Composition.single n hn).length) ↦
    (p n : (a : (i : Fin n) → E) → F) v
have 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
Tactic: ext j
-- 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 : ℕ
hn : 0 < n
v : Fin n → E
j : Fin (Composition.single n hn).length
⊢ p.applyComposition (Composition.single n hn) v j = (p n : (a : (i : Fin n) → E) → F) v
have 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⟩
Tactic: refine p.congr (by simp) fun i hi1 hi2 => ?_
-- 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 : ℕ
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
⊢ (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⟩
have 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⟩
Tactic: dsimp
-- 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 : ℕ
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
⊢ 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⟩
have h : ((Composition.single n hn).embedding j : (a : Fin ((Composition.single n hn).blocksFun j)) → Fin n) ⟨i, hi1⟩ =
  (⟨i, hi2⟩ : Fin n)
Tactic: congr 1
-- 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 : ℕ
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 j : (a : Fin ((Composition.single n hn).blocksFun j)) → Fin n) ⟨i, hi1⟩ =
    (⟨i, hi2⟩ : Fin n)
have 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)
Tactic: convert! Composition.single_embedding hn ⟨i, hi2⟩ using 1
-- 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 : ℕ
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
⊢ 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)
have 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)
Tactic: obtain ⟨j_val, j_property⟩ := j
Cleared hypotheses: j, hi1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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⟩
⊢ 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)
have this : j_val = 0
Tactic: have : j_val = 0 := le_bot_iff.1 (Nat.lt_succ_iff.1 j_property)
-- 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 : ℕ
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 ⟨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)
have h : Eq (α := Fin n)
  (((Composition.single n hn).embedding ⟨0, sorry⟩ : (a : Fin ((Composition.single n hn).blocksFun ⟨0, sorry⟩)) → Fin n)
      ⟨i, sorry⟩ :
    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]
-- 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 : ℕ
c : Composition n
⊢ p.removeZero.applyComposition c = p.applyComposition c
have h : ∀ (v : Fin n → E) (i : Fin c.length), p.removeZero.applyComposition c v i = p.applyComposition c v i
Tactic: ext 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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
⊢ 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))
have 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
Tactic: ext k
-- 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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
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
have 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
Tactic: by_cases h : k = c.index j
-- 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 : ℕ
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
⊢ 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
have 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
Tactic: by_cases h : k = c.index j
-- 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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
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
have pos : p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) (c.index j) =
  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))
    (c.index j)
Tactic: rw [h]
-- 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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
r : Fin (c.blocksFun (c.index j)) → Fin n := (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)
⊢ p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) (c.index j) =
    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))
      (c.index j)
have pos : p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) (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: simp only [Function.update_self]
-- 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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
r : Fin (c.blocksFun (c.index j)) → Fin n := (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)
⊢ p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) (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)
have pos : Eq.{u_3 + 1} (α := F)
  ((p (c.blocksFun (c.index j)) : (a : (i : Fin (c.blocksFun (c.index j))) → E) → F)
      (Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r) :
    F)
  ((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) :
    F)
Tactic: change p (c.blocksFun (c.index j)) (Function.update v j z ∘ r) = _
-- 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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
r : Fin (c.blocksFun (c.index j)) → Fin n := (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)
j' : Fin (c.blocksFun (c.index j)) := c.invEmbedding j
B :
  Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r =
    Function.update (β := fun (a : Fin (c.blocksFun (c.index j))) ↦ E) (v ∘ r) j' z
⊢ Eq.{u_3 + 1} (α := F)
    ((p (c.blocksFun (c.index j)) : (a : (i : Fin (c.blocksFun (c.index j))) → E) → F)
        (Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r) :
      F)
    ((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) :
      F)
have rw : Eq.{u_3 + 1} (α := F)
  ((p (c.blocksFun (c.index j)) : (a : (i : Fin (c.blocksFun (c.index j))) → E) → F)
      (Function.update (β := fun (a : Fin (c.blocksFun (c.index j))) ↦ E) (v ∘ r) j' z) :
    F)
  ((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) :
    F)
Tactic: rw [B]
-- 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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
r : Fin (c.blocksFun (c.index j)) → Fin n := (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)
j' : Fin (c.blocksFun (c.index j)) := c.invEmbedding j
⊢ Eq.{u_3 + 1} (α := F)
    ((p (c.blocksFun (c.index j)) : (a : (i : Fin (c.blocksFun (c.index j))) → E) → F)
        (Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r) :
      F)
    ((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) :
      F)
have pos : Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r =
  Function.update (β := fun (a : Fin (c.blocksFun (c.index j))) ↦ E) (v ∘ r) j' z
Tactic: suffices B : Function.update v j z ∘ r = Function.update (v ∘ r) j' z by rw [B]
-- 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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
r : Fin (c.blocksFun (c.index j)) → Fin n := (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)
j' : Fin (c.blocksFun (c.index j)) := c.invEmbedding j
C :
  Function.update (β := fun (a : Fin n) ↦ E) v (r j') z ∘ r =
    Function.update (β := fun (a : Fin (c.blocksFun (c.index j))) ↦ E) (v ∘ r) j' z
⊢ Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r =
    Function.update (β := fun (a : Fin (c.blocksFun (c.index j))) ↦ E) (v ∘ r) j' z
have h₁ : j = r j'
Tactic: convert! C