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
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
⊢ Eq (α := FormalMultilinearSeries 𝕜 E G) (q.comp p.removeZero : FormalMultilinearSeries 𝕜 E G)
    (q.comp p : FormalMultilinearSeries 𝕜 E G)
have h : ∀ (n : ℕ) (x : (i : Fin n) → E),
  Eq.{u_4 + 1} (α := G) ((q.comp p.removeZero n : (a : (i : Fin n) → E) → G) x : G)
    ((q.comp p n : (a : (i : Fin n) → E) → G) x : G)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
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 : Fin n → E
⊢ ‖f‖ * ∏ i : Fin c.length, ‖p.applyComposition c v i‖ ≤
    ‖f‖ *
      ∏ i : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i)) *
          ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖
have hbc : ∀ (i : Fin c.length),
  Membership.mem (γ := Finset (Fin c.length)) Finset.univ i →
    ‖p.applyComposition c v i‖ ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
          (p (c.blocksFun i)) *
        ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖
Tactic: gcongr with i
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
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 : Fin n → E
⊢ ‖f‖ *
      ∏ i : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i)) *
          ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖ =
    (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖
have rw : ‖f‖ *
    HMul.hMul (α := ℝ)
      (∏ x : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun x)) ↦ E) F)
          (p (c.blocksFun x)))
      (∏ x : Fin c.length,
        ∏ j : Fin (c.blocksFun x), ‖(v ∘ (⇑(c.embedding x) : (a : Fin (c.blocksFun x)) → Fin n)) j‖) =
  (‖f‖ *
      ∏ i : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
          (p (c.blocksFun i))) *
    ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖
Tactic: rw [Finset.prod_mul_distrib, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
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 : Fin n → E
rw :
  ‖f‖ *
      HMul.hMul (α := ℝ)
        (∏ x : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun x)) ↦ E) F)
            (p (c.blocksFun x)))
        (∏ x : Fin c.length,
          ∏ j : Fin (c.blocksFun x), ‖(v ∘ (⇑(c.embedding x) : (a : Fin (c.blocksFun x)) → Fin n)) j‖) =
    (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖
⊢ ‖f‖ *
      ∏ i : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i)) *
          ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖ =
    (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖
have rw₁ : ‖f‖ *
    HMul.hMul (α := ℝ)
      (∏ x : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun x)) ↦ E) F)
          (p (c.blocksFun x)))
      (∏ x : Fin c.length,
        ∏ j : Fin (c.blocksFun x), ‖(v ∘ (⇑(c.embedding x) : (a : Fin (c.blocksFun x)) → Fin n)) j‖) =
  ‖f‖ *
    HMul.hMul (α := ℝ)
      (∏ i : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
          (p (c.blocksFun i)))
      (∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖)
Tactic: rw [Finset.prod_mul_distrib, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
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 : Fin n → E
⊢ (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖ =
    (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ i : Fin n, ‖v i‖
have rw : (‖f‖ *
      ∏ i : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
          (p (c.blocksFun i))) *
    ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖ =
  (‖f‖ *
      ∏ i : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
          (p (c.blocksFun i))) *
    ∏ a : Fin c.length,
      ∏ s : Fin (c.blocksFun a),
        ‖v
            ((c.blocksFinEquiv : (a : (i : Fin c.length) × Fin (c.blocksFun i)) → Fin n)
              (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) a s))‖
Tactic: rw [← c.blocksFinEquiv.prod_comp, ← Finset.univ_sigma_univ, Finset.prod_sigma]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ (↑‖q.compAlongComposition p c‖₊ : ℝ) ≤
    (↑(nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) *
          ∏ i : Fin c.length,
            nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
              (p (c.blocksFun i))) :
      ℝ)
have push_cast : ‖q.compAlongComposition p c‖ ≤
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) *
    ∏ x : Fin c.length,
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun x)) ↦ E) F)
        (p (c.blocksFun x))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
h : n = 1
v : Fin n → E
⊢ (id 𝕜 E x n : (a : (i : Fin n) → E) → E) v = v (⟨0, ⋯⟩ : Fin n)
have subst : ∀ (v : Fin 1 → E), (id 𝕜 E x 1 : (a : (i : Fin 1) → E) → E) v = v (⟨0, sorry⟩ : Fin 1)
Tactic: subst n
Cleared hypotheses: n, h, v
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
⊢ p.comp (id 𝕜 E x) = p
have h : ∀ (n : ℕ), p.comp (id 𝕜 E x) n = p n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
⊢ ∑ c : Composition n, p.compAlongComposition (id 𝕜 E x) c = p n
have h : p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = p n
Tactic: rw [Finset.sum_eq_single (Composition.ones n)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
h : p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = p n
⊢ ∑ c : Composition n, p.compAlongComposition (id 𝕜 E x) c = p n
have h₁ : ∀ (b : Composition n),
  Membership.mem (γ := Finset (Composition n)) Finset.univ b →
    b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E x) b = 0
Tactic: rw [Finset.sum_eq_single (Composition.ones n)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
h : p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = p n
h₁ :
  ∀ (b : Composition n),
    Membership.mem (γ := Finset (Composition n)) Finset.univ b →
      b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E x) b = 0
⊢ ∑ c : Composition n, p.compAlongComposition (id 𝕜 E x) c = p n
have h₂ : Composition.ones n ∉ Finset.univ → p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = 0
Tactic: rw [Finset.sum_eq_single (Composition.ones n)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
⊢ p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = p n
have h : ∀ (v : (i : Fin n) → E),
  Eq.{u_3 + 1} (α := F) ((p.compAlongComposition (id 𝕜 E x) (Composition.ones n) : (a : (i : Fin n) → E) → F) v : F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F) ((p.compAlongComposition (id 𝕜 E x) (Composition.ones n) : (a : (i : Fin n) → E) → F) v : F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)
have h : Eq.{u_3 + 1} (α := F)
  ((p (Composition.ones n).length : (a : (i : Fin (Composition.ones n).length) → E) → F)
      (applyComposition (id 𝕜 E x) (Composition.ones n) v) :
    F)
  ((p n : (a : (i : Fin n) → E) → F) v : F)
Tactic: rw [compAlongComposition_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((p (Composition.ones n).length : (a : (i : Fin (Composition.ones n).length) → E) → F)
        (applyComposition (id 𝕜 E x) (Composition.ones n) v) :
      F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)
have h : ∀ (i : ℕ) (him : i < (Composition.ones n).length) (hin : i < n),
  applyComposition (id 𝕜 E x) (Composition.ones n) v (⟨i, him⟩ : Fin (Composition.ones n).length) = v ⟨i, hin⟩
Tactic: apply p.congr (Composition.ones_length n)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.ones n).length
hin : i < n
⊢ applyComposition (id 𝕜 E x) (Composition.ones n) v (⟨i, him⟩ : Fin (Composition.ones n).length) = v ⟨i, hin⟩
have h : (fun (v : Fin n → E) (i : Fin (Composition.ones n).length) ↦
      ((id 𝕜 E x 1 : (a : (i : Fin 1) → E) → E) fun (x : Fin 1) ↦ v (Fin.castLE sorry i) : E))
    v ⟨i, him⟩ =
  v (⟨i, hin⟩ : Fin n)
Tactic: rw [applyComposition_ones]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.ones n).length
hin : i < n
⊢ (fun (v : Fin n → E) (i : Fin (Composition.ones n).length) ↦
        ((id 𝕜 E x 1 : (a : (i : Fin 1) → E) → E) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ i) : E))
      v ⟨i, him⟩ =
    v (⟨i, hin⟩ : Fin n)
have h : Fin.castLE sorry (⟨i, him⟩ : Fin (Composition.ones n).length) = ⟨i, hin⟩
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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.ones n).length
hin : i < n
⊢ Fin.castLE ⋯ (⟨i, him⟩ : Fin (Composition.ones n).length) = ⟨i, hin⟩
have h : (↑(Fin.castLE sorry (⟨i, him⟩ : Fin (Composition.ones n).length)) : ℕ) = (↑(⟨i, hin⟩ : Fin n) : ℕ)
Tactic: rw [Fin.ext_iff, Fin.val_castLE, 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.ones n).length
hin : i < n
h : (↑(Fin.castLE ⋯ (⟨i, him⟩ : Fin (Composition.ones n).length)) : ℕ) = (↑(⟨i, hin⟩ : Fin n) : ℕ)
⊢ Fin.castLE ⋯ (⟨i, him⟩ : Fin (Composition.ones n).length) = ⟨i, hin⟩
have h₁ : (↑(⟨i, him⟩ : Fin (Composition.ones n).length) : ℕ) = (↑(⟨i, hin⟩ : Fin n) : ℕ)
Tactic: rw [Fin.ext_iff, Fin.val_castLE, 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.ones n).length
hin : i < n
h : (↑(Fin.castLE ⋯ (⟨i, him⟩ : Fin (Composition.ones n).length)) : ℕ) = (↑(⟨i, hin⟩ : Fin n) : ℕ)
h₁ : (↑(⟨i, him⟩ : Fin (Composition.ones n).length) : ℕ) = (↑(⟨i, hin⟩ : Fin n) : ℕ)
⊢ Fin.castLE ⋯ (⟨i, him⟩ : Fin (Composition.ones n).length) = ⟨i, hin⟩
have h₂ : i = i
Tactic: rw [Fin.ext_iff, Fin.val_castLE, 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
⊢ p.compAlongComposition (id 𝕜 E x) b = 0
have h : ∀ (k : ℕ) (hk : k ∈ b.blocks) (lt_k : 1 < k), p.compAlongComposition (id 𝕜 E x) b = 0
Tactic: obtain ⟨k, hk, lt_k⟩ : ∃ (k : ℕ), k ∈ Composition.blocks b ∧ 1 < k :=
      Composition.ne_ones_iff.1 hb
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
⊢ p.compAlongComposition (id 𝕜 E x) b = 0
have h : ∀ (i : Fin b.blocks.length)
  (hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i sorry = k),
  p.compAlongComposition (id 𝕜 E x) b = 0
Tactic: obtain ⟨i, hi⟩ : ∃ (i : Fin b.blocks.length), b.blocks[i] = k :=
      List.get_of_mem hk
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
⊢ p.compAlongComposition (id 𝕜 E x) b = 0
have A : 1 < b.blocksFun j
Tactic: have A : 1 < b.blocksFun j := by convert! lt_k
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
A : 1 < b.blocksFun j
⊢ p.compAlongComposition (id 𝕜 E x) b = 0
have h : ∀ (v : (i : Fin n) → E),
  Eq.{u_3 + 1} (α := F) ((p.compAlongComposition (id 𝕜 E x) b : (a : (i : Fin n) → E) → F) v : F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
A : 1 < b.blocksFun j
v : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F) ((p.compAlongComposition (id 𝕜 E x) b : (a : (i : Fin n) → E) → F) v : F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)
have h : Eq.{u_3 + 1} (α := F) ((p b.length : (a : (i : Fin b.length) → E) → F) (applyComposition (id 𝕜 E x) b v) : F) (0 : F)
Tactic: rw [compAlongComposition_apply, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
A : 1 < b.blocksFun j
v : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F) ((p b.length : (a : (i : Fin b.length) → E) → F) (applyComposition (id 𝕜 E x) b v) : F) (0 : F)
have h : applyComposition (id 𝕜 E x) b v j = 0
Tactic: apply ContinuousMultilinearMap.map_coord_zero _ j
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
A : 1 < b.blocksFun j
v : (i : Fin n) → E
⊢ applyComposition (id 𝕜 E x) b v j = 0
have h : Eq (α := E)
  ((id 𝕜 E x (b.blocksFun j) : (a : (i : Fin (b.blocksFun j)) → E) → E)
      (v ∘ (⇑(b.embedding j) : (a : Fin (b.blocksFun j)) → Fin n)) :
    E)
  (0 : E)
Tactic: dsimp [applyComposition]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
A : 1 < b.blocksFun j
v : (i : Fin n) → E
⊢ Eq (α := E)
    ((id 𝕜 E x (b.blocksFun j) : (a : (i : Fin (b.blocksFun j)) → E) → E)
        (v ∘ (⇑(b.embedding j) : (a : Fin (b.blocksFun j)) → Fin n)) :
      E)
    (0 : E)
have h : Eq (α := E)
  ((0 : (a : (i : Fin (b.blocksFun j)) → E) → E) (v ∘ (⇑(b.embedding j) : (a : Fin (b.blocksFun j)) → Fin n)) : E)
  (0 : E)
Tactic: rw [id_apply_of_one_lt _ _ _ A, ContinuousMultilinearMap.zero_apply]