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 : 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_1 : 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
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)
⊢ 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.{u_2 + 1} (α := E) 0 0
Tactic: rw [id_apply_of_one_lt _ _ _ A, 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
v0 : Fin 0 → E
⊢ FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p = p
have h : ∀ (n : ℕ), FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 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
v0 : Fin 0 → E
n : ℕ
⊢ FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p n = p n
have h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
  (FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 0) (p 0)
Tactic: obtain rfl | n_pos := n.eq_zero_or_pos
Cleared hypotheses: 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
v0 : Fin 0 → E
n : ℕ
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 0) (p 0)
⊢ FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p n = p n
have h₁ : ∀ (n_pos : n > 0), FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p n = p n
Tactic: obtain rfl | n_pos := n.eq_zero_or_pos
-- 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
v0 : Fin 0 → E
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 0) (p 0)
have h : ∀ (v : (i : Fin 0) → E),
  Eq.{u_3 + 1} (α := F)
    ((FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 0 : (a : (i : Fin 0) → E) → F) v :
      F)
    ((p 0 : (a : (i : Fin 0) → 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
v0 v : (i : Fin 0) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 0 : (a : (i : Fin 0) → E) → F) v :
      F)
    ((p 0 : (a : (i : Fin 0) → E) → F) v : F)
have h : Eq.{u_3 + 1} (α := F) ((p 0 : (a : (i : Fin 0) → E) → F) v0 : F) ((p 0 : (a : (i : Fin 0) → E) → F) v : F)
Tactic: simp only [comp_coeff_zero', id_apply_zero]
-- 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
v0 v : (i : Fin 0) → E
⊢ Eq.{u_3 + 1} (α := F) ((p 0 : (a : (i : Fin 0) → E) → F) v0 : F) ((p 0 : (a : (i : Fin 0) → E) → F) v : F)
have h : ∀ (i : Fin 0), v0 i = v i
Tactic: congr with i
-- 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ ∑ c : Composition n, compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p c = p n
have h : compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) = p n
Tactic: rw [Finset.sum_eq_single (Composition.single n n_pos)]
-- 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
h : compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) = p n
⊢ ∑ c : Composition n, compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p c = p n
have h₁ : ∀ (b : Composition n),
  Membership.mem (γ := Finset (Composition n)) Finset.univ b →
    b ≠ Composition.single n n_pos → compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b = 0
Tactic: rw [Finset.sum_eq_single (Composition.single n n_pos)]
-- 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
h : compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) = p n
h₁ :
  ∀ (b : Composition n),
    Membership.mem (γ := Finset (Composition n)) Finset.univ b →
      b ≠ Composition.single n n_pos → compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b = 0
⊢ ∑ c : Composition n, compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p c = p n
have h₂ : Composition.single n n_pos ∉ Finset.univ →
  compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) = 0
Tactic: rw [Finset.sum_eq_single (Composition.single n n_pos)]
-- 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) = p n
have h : ∀ (v : (i : Fin n) → E),
  Eq.{u_3 + 1} (α := F)
    ((compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) :
          (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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) :
          (a : (i : Fin n) → E) → F)
        v :
      F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)
have h : p.applyComposition (Composition.single n n_pos) v (⟨0, sorry⟩ : Fin (Composition.single n n_pos).length) =
  (p n : (a : (i : Fin n) → E) → F) v
Tactic: rw [compAlongComposition_apply, id_apply_one' _ _ _ (Composition.single_length n_pos)]
-- 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : (i : Fin n) → E
⊢ p.applyComposition (Composition.single n n_pos) v (⟨0, ⋯⟩ : Fin (Composition.single n n_pos).length) =
    (p n : (a : (i : Fin n) → E) → F) v
have h : Eq.{u_3 + 1} (α := F)
  ((p ((Composition.single n n_pos).blocksFun 0) : (a : (i : Fin ((Composition.single n n_pos).blocksFun 0)) → E) → F)
      (v ∘
        (⇑((Composition.single n n_pos).embedding 0) : (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n)) :
    F)
  ((p n : (a : (i : Fin n) → E) → F) v : F)
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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((p ((Composition.single n n_pos).blocksFun 0) : (a : (i : Fin ((Composition.single n n_pos).blocksFun 0)) → E) → F)
        (v ∘
          (⇑((Composition.single n n_pos).embedding 0) :
            (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n)) :
      F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)
have h : ∀ (i : ℕ) (him : i < (Composition.single n n_pos).blocksFun 0) (hin : i < n),
  ((Composition.single n n_pos).embedding 0 : (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n) ⟨i, him⟩ =
    (⟨i, hin⟩ : Fin n)
Tactic: refine p.congr rfl fun i him hin => 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.single n n_pos).blocksFun 0
hin : i < n
⊢ ((Composition.single n n_pos).embedding 0 : (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n) ⟨i, him⟩ =
    (⟨i, hin⟩ : Fin n)
have h : (↑(((Composition.single n n_pos).embedding 0 : (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n)
        (⟨i, him⟩ : Fin ((Composition.single n n_pos).blocksFun 0))) :
    ℕ) =
  (↑(⟨i, hin⟩ : Fin n) : ℕ)
Tactic: ext
-- 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
⊢ 1 < b.length
have this : b.length ≠ 1
Tactic: have : b.length ≠ 1 := by simpa [Composition.eq_single_iff_length] using hb
-- 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
this : b.length ≠ 1
⊢ 1 < b.length
have this₁ : 0 < b.length
Tactic: have : 0 < b.length := Composition.length_pos_of_pos b n_pos
-- 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
⊢ compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b = 0
have A : 1 < b.length
Tactic: have A : 1 < b.length := by
        have : b.length ≠ 1 := by simpa [Composition.eq_single_iff_length] using hb
        have : 0 < b.length := Composition.length_pos_of_pos b n_pos
        lia
-- 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
⊢ compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b = 0
have h : ∀ (v : (i : Fin n) → E),
  Eq.{u_3 + 1} (α := F)
    ((compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
v : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b : (a : (i : Fin n) → E) → F) v : F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)
have h : Eq (α := F)
  ((id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0) b.length : (a : (i : Fin b.length) → F) → F)
      (p.applyComposition b v) :
    F)
  ((0 : (a : (i : Fin n) → E) → F) v : F)
Tactic: rw [compAlongComposition_apply, id_apply_of_one_lt _ _ _ A,
        ContinuousMultilinearMap.zero_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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
v : (i : Fin n) → E
h :
  Eq (α := F)
    ((id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0) b.length : (a : (i : Fin b.length) → F) → F)
        (p.applyComposition b v) :
      F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)
⊢ Eq.{u_3 + 1} (α := F)
    ((compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b : (a : (i : Fin n) → E) → F) v : F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)
have h₁ : Eq (α := F) ((0 : (a : (i : Fin b.length) → F) → F) (p.applyComposition b v) : F)
  ((0 : (a : (i : Fin n) → E) → F) v : F)
Tactic: rw [compAlongComposition_apply, id_apply_of_one_lt _ _ _ A,
        ContinuousMultilinearMap.zero_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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
v : (i : Fin n) → E
h :
  Eq (α := F)
    ((id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0) b.length : (a : (i : Fin b.length) → F) → F)
        (p.applyComposition b v) :
      F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)
h₁ :
  Eq (α := F) ((0 : (a : (i : Fin b.length) → F) → F) (p.applyComposition b v) : F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)
⊢ Eq.{u_3 + 1} (α := F)
    ((compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 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) (0 : F) ((0 : (a : (i : Fin n) → E) → F) v : F)
Tactic: rw [compAlongComposition_apply, id_apply_of_one_lt _ _ _ A,
        ContinuousMultilinearMap.zero_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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
v : (i : Fin n) → E
h :
  Eq (α := F)
    ((id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0) b.length : (a : (i : Fin b.length) → F) → F)
        (p.applyComposition b v) :
      F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)
h₁ :
  Eq (α := F) ((0 : (a : (i : Fin b.length) → F) → F) (p.applyComposition b v) : F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)
h₂ : Eq.{u_3 + 1} (α := F) (0 : F) ((0 : (a : (i : Fin n) → E) → F) v : F)
⊢ Eq.{u_3 + 1} (α := F)
    ((compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 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) 0 0
Tactic: rw [compAlongComposition_apply, id_apply_of_one_lt _ _ _ A,
        ContinuousMultilinearMap.zero_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
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
⊢ ∃ r > 0,
    Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
have rcases : ∀ (rq : ℝ≥0) (rq_pos : 0 < (↑rq : ℝ≥0∞)) (hrq : (↑rq : ℝ≥0∞) < min 1 q.radius),
  ∃ r > 0,
    Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
Tactic: rcases ENNReal.lt_iff_exists_nnreal_btwn.1 (lt_min zero_lt_one hq) with ⟨rq, rq_pos, hrq⟩
-- 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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq : ℝ≥0
rq_pos : 0 < (↑rq : ℝ≥0∞)
hrq : (↑rq : ℝ≥0∞) < min 1 q.radius
⊢ ∃ r > 0,
    Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
have rcases : ∀ (rp : ℝ≥0) (rp_pos : 0 < (↑rp : ℝ≥0∞)) (hrp : (↑rp : ℝ≥0∞) < min 1 p.radius),
  ∃ r > 0,
    Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
Tactic: rcases ENNReal.lt_iff_exists_nnreal_btwn.1 (lt_min zero_lt_one hp) with ⟨rp, rp_pos, hrp⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq : ℝ≥0
rq_pos : 0 < (↑rq : ℝ≥0∞)
hrq : (↑rq : ℝ≥0∞) < min 1 q.radius
rp : ℝ≥0
rp_pos : 0 < (↑rp : ℝ≥0∞)
hrp : (↑rp : ℝ≥0∞) < min 1 p.radius
⊢ ∃ r > 0,
    Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
have hrp₁ : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
Tactic: simp only [lt_min_iff, ENNReal.coe_lt_one_iff, ENNReal.coe_pos] at hrp hrq rp_pos rq_pos
Cleared hypotheses: rq_pos, hrq, rp_pos, hrp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq : ℝ≥0
rq_pos : 0 < (↑rq : ℝ≥0∞)
hrq : (↑rq : ℝ≥0∞) < min 1 q.radius
rp : ℝ≥0
rp_pos : 0 < (↑rp : ℝ≥0∞)
hrp : (↑rp : ℝ≥0∞) < min 1 p.radius
hrp₁ : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
⊢ ∃ r > 0,
    Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
have hrq₁ : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
Tactic: simp only [lt_min_iff, ENNReal.coe_lt_one_iff, ENNReal.coe_pos] at hrp hrq rp_pos rq_pos
Cleared hypotheses: rq_pos, hrq, rp_pos, hrp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq : ℝ≥0
rq_pos : 0 < (↑rq : ℝ≥0∞)
hrq : (↑rq : ℝ≥0∞) < min 1 q.radius
rp : ℝ≥0
rp_pos : 0 < (↑rp : ℝ≥0∞)
hrp : (↑rp : ℝ≥0∞) < min 1 p.radius
hrp₁ : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq₁ : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
⊢ ∃ r > 0,
    Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
have rp_pos₁ : 0 < rp
Tactic: simp only [lt_min_iff, ENNReal.coe_lt_one_iff, ENNReal.coe_pos] at hrp hrq rp_pos rq_pos
Cleared hypotheses: rq_pos, hrq, rp_pos, hrp