awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : k = c.index j
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)
⊢ 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:
rw [h]
-- 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
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)
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)
⊢ 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:
simp only [Function.update_self]

Premises used: Function.update_self
-- 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
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)
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)
⊢ 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:
change p (c.blocksFun (c.index j)) (Function.update v j z ∘ r) = _

Premises used: Function.update, Composition.blocksFun, Function.comp, Composition.index, DFunLike.coe
-- 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
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
rw 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)
⊢ 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:
rw [B]
-- 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
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
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
⊢ 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:
suffices B : Function.update v j z ∘ r = Function.update (v ∘ r) j' z by rw [B]
-- 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
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 (r j') z ∘ r =
    Function.update (β := fun (a : Fin (c.blocksFun (c.index j))) ↦ E) (v ∘ r) j' z

Tactic:
C
-- 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
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
h₁ : j = r j'
⊢ 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:
convert! C
-- 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
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
⊢ j = r j'

Tactic:
(c.embedding_comp_inv j).symm

Premises used: Composition.embedding_comp_inv, Eq.symm
-- 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
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
⊢ j = r j'

Tactic:
exact (c.embedding_comp_inv j).symm

Premises used: Composition.embedding_comp_inv, Eq.symm
-- 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
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
pos :
  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

Tactic:
suffices C : Function.update v (r j') z ∘ r = Function.update (v ∘ r) j' z by
      convert! C; exact (c.embedding_comp_inv j).symm
-- 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
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
⊢ 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

Tactic:
Function.update_comp_eq_of_injective _ (c.embedding _).injective _ _

Premises used: RelEmbedding.injective, Composition.embedding, Function.update_comp_eq_of_injective
-- 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
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
⊢ 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

Tactic:
exact Function.update_comp_eq_of_injective _ (c.embedding _).injective _ _

Premises used: RelEmbedding.injective, Composition.embedding, Function.update_comp_eq_of_injective
-- 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
h : ¬k = c.index j
neg : p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) k = p.applyComposition c v 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:
simp only [h, Function.update_of_ne, Ne, not_false_iff]

Premises used: Ne, not_false_iff, Function.update_of_ne
-- 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
h : ¬k = c.index j
r : Fin (c.blocksFun k) → Fin n := (⇑(c.embedding k) : (a : Fin (c.blocksFun k)) → Fin n)
neg :
  Eq.{u_3 + 1} (α := F)
    ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F)
        (Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r) :
      F)
    ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F) (v ∘ r) : F)
⊢ p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) k = p.applyComposition c v k

Tactic:
change p (c.blocksFun k) (Function.update v j z ∘ r) = p (c.blocksFun k) (v ∘ r)

Premises used: Function.update, Composition.blocksFun, Function.comp, DFunLike.coe
-- 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
h : ¬k = c.index j
r : Fin (c.blocksFun k) → Fin n := (⇑(c.embedding k) : (a : Fin (c.blocksFun k)) → Fin n)
B : Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r = v ∘ r
rw rw₁ :
  Eq.{u_3 + 1} (α := F) ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F) (v ∘ r) : F)
    ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F) (v ∘ r) : F)
⊢ Eq.{u_3 + 1} (α := F)
    ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F)
        (Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r) :
      F)
    ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F) (v ∘ r) : F)

Tactic:
rw [B]
-- 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
h : ¬k = c.index j
r : Fin (c.blocksFun k) → Fin n := (⇑(c.embedding k) : (a : Fin (c.blocksFun k)) → Fin n)
neg : Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r = v ∘ r
⊢ Eq.{u_3 + 1} (α := F)
    ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F)
        (Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r) :
      F)
    ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F) (v ∘ r) : F)

Tactic:
suffices B : Function.update v j z ∘ r = v ∘ r by rw [B]
-- 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
h : ¬k = c.index j
r : Fin (c.blocksFun k) → Fin n := (⇑(c.embedding k) : (a : Fin (c.blocksFun k)) → Fin n)
neg : j ∉ Set.range r
⊢ Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r = v ∘ r

Tactic:
apply Function.update_comp_eq_of_notMem_range

Premises used: Function.update_comp_eq_of_notMem_range
-- 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
h : ¬k = c.index j
r : Fin (c.blocksFun k) → Fin n := (⇑(c.embedding k) : (a : Fin (c.blocksFun k)) → Fin n)
neg neg₁ neg₂ neg₃ : ¬k = c.index j
⊢ j ∉ Set.range r

Tactic:
rwa [c.mem_range_embedding_iff']

Premises used: Composition.mem_range_embedding_iff'
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
n : ℕ
p : FormalMultilinearSeries 𝕜 F G
f : E →L[𝕜] F
c : Composition n
v : Fin n → E
h :
  ∀ (x : Fin c.length),
    applyComposition (p.compContinuousLinearMap f) c v x = p.applyComposition c ((⇑f : (a : E) → F) ∘ v) x
⊢ applyComposition (p.compContinuousLinearMap f) c v = p.applyComposition c ((⇑f : (a : E) → F) ∘ v)

Tactic:
ext
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
n : ℕ
p : FormalMultilinearSeries 𝕜 F G
f : E →L[𝕜] F
c : Composition n
v : Fin n → E
x : Fin c.length
⊢ applyComposition (p.compContinuousLinearMap f) c v x = p.applyComposition c ((⇑f : (a : E) → F) ∘ v) x

Tactic:
simp [applyComposition, Function.comp_def]

Premises used: FormalMultilinearSeries.applyComposition, Function.comp_def
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
v : (i : Fin n) → E
i : Fin n
x y : E
⊢ (fun (v : (i : Fin n) → E) ↦ ((f : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G))
      (Function.update (β := fun (i : Fin n) ↦ E) v i (x + y)) =
    HAdd.hAdd (α := G)
      ((fun (v : (i : Fin n) → E) ↦ ((f : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G))
        (Function.update (β := fun (i : Fin n) ↦ E) v i x))
      ((fun (v : (i : Fin n) → E) ↦ ((f : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G))
        (Function.update (β := fun (i : Fin n) ↦ E) v i y))

Tactic:
simp only [applyComposition_update, map_update_add]

Premises used: ContinuousMultilinearMap.map_update_add, FormalMultilinearSeries.applyComposition_update