awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
H : u = v
⊢ Eq (α := List (List ℕ))
    (ofFn (n := u.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
      fun (i : Fin u.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (u.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).blocks)
    (ofFn (n := v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
      fun (i : Fin v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (v.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).blocks)
have rw : Eq (α := List (List ℕ))
  (ofFn (n := v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
    fun (i : Fin v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
    (v.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).blocks)
  (ofFn (n := v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
    fun (i : Fin v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
    (v.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).blocks)
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
⊢ u = v ↔
    Eq (α := List (List ℕ))
      (ofFn (n := u.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
        fun (i : Fin u.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
        (u.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).blocks)
      (ofFn (n := v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
        fun (i : Fin v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
        (v.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).blocks)
have refine : ∀
  (H :
    Eq (α := List (List ℕ))
      (ofFn (n := u.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
        fun (i : Fin u.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
        (u.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).blocks)
      (ofFn (n := v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
        fun (i : Fin v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
        (v.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).blocks)),
  u = v
Tactic: refine ⟨fun H => by rw [H], fun H => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
H :
  Eq (α := List (List ℕ))
    (ofFn (n := u.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
      fun (i : Fin u.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (u.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).blocks)
    (ofFn (n := v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
      fun (i : Fin v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (v.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).blocks)
⊢ u = v
have rcases : ∀ (a : Composition n) (b : (i : Fin a.length) → Composition (a.blocksFun i))
  (H :
    Eq (α := List (List ℕ))
      (ofFn (n :=
        (Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
            (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b)).length)
        fun
          (i :
            Fin
              (Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                  (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a
                    b)).length) ↦
        blocks (n :=
          (Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a
                  b)).blocksFun
            i)
          (Sigma.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
            (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b) i))
      (ofFn (n := v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
        fun (i : Fin v.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
        (v.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) i).blocks)),
  Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b = v
Tactic: rcases u with ⟨a, b⟩
Cleared hypotheses: u, H
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H :
  Eq (α := List (List ℕ)) (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks)
    (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks)
⊢ a = a'
have blocks : a.blocks = a'.blocks
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H :
  Eq (α := List (List ℕ)) (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks)
    (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks)
⊢ Eq (α := List ℕ) (List.map sum (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks))
    (List.map sum (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks))
have rw : Eq (α := List ℕ) (List.map sum (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks))
  (List.map sum (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks))
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H :
  Eq (α := List (List ℕ)) (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks)
    (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks)
⊢ a.blocks = a'.blocks
have this : Eq (α := List ℕ) (List.map sum (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks))
  (List.map sum (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks))
Tactic: have :
      map List.sum (ofFn fun i : Fin (Composition.length a) => (b i).blocks) =
        map List.sum (ofFn fun i : Fin (Composition.length a') => (b' i).blocks) := by
      rw [H]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H :
  Eq (α := List (List ℕ)) (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks)
    (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks)
this :
  Eq (α := List ℕ) (List.map sum (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks))
    (List.map sum (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks))
⊢ a.blocks = a'.blocks
have this₁ : Eq (α := List ℕ) (ofFn (n := a.length) (sum ∘ fun (i : Fin a.length) ↦ (b i).blocks))
  (ofFn (n := a'.length) (sum ∘ fun (i : Fin a'.length) ↦ (b' i).blocks))
Tactic: simp only [map_ofFn] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H :
  Eq (α := List (List ℕ)) (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks)
    (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks)
this :
  Eq (α := List ℕ) (ofFn (n := a.length) (sum ∘ fun (i : Fin a.length) ↦ (b i).blocks))
    (ofFn (n := a'.length) (sum ∘ fun (i : Fin a'.length) ↦ (b' i).blocks))
⊢ a.blocks = a'.blocks
have this₁ : Eq (α := List ℕ) (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks.sum)
  (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks.sum)
Tactic: change
      (ofFn fun i : Fin (Composition.length a) => (b i).blocks.sum) =
        ofFn fun i : Fin (Composition.length a') => (b' i).blocks.sum at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H :
  Eq (α := List (List ℕ)) (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks)
    (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks)
⊢ Eq (α := (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)))
    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b)
    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a' b')
have obtain : ∀ (b' : (i : Fin a.length) → Composition (a.blocksFun i))
  (H :
    Eq (α := List (List ℕ)) (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks)
      (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b' i).blocks)),
  Eq (α := (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)))
    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b)
    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b')
Tactic: obtain rfl : a = a' := by
    ext1
    have :
      map List.sum (ofFn fun i : Fin (Composition.length a) => (b i).blocks) =
        map List.sum (ofFn fun i : Fin (Composition.length a') => (b' i).blocks) := by
      rw [H]
    simp only [map_ofFn] at this
    change
      (ofFn fun i : Fin (Composition.length a) => (b i).blocks.sum) =
        ofFn fun i : Fin (Composition.length a') => (b' i).blocks.sum at this
    simpa [Composition.blocks_sum, Composition.ofFn_blocksFun] using this
Cleared hypotheses: a', b', H
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H :
  Eq (α := List (List ℕ)) (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks)
    (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b' i).blocks)
⊢ Eq (α := (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)))
    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b)
    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b')
have fst : Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b) =
  Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
    (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b')
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H :
  Eq (α := List (List ℕ)) (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b i).blocks)
    (ofFn (n := a.length) fun (i : Fin a.length) ↦ (b' i).blocks)
⊢ HEq (α :=
    (i :
        Fin
          (Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
              (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a
                b)).length) →
      Composition
        ((Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
              (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a
                b)).blocksFun
          i))
    (Sigma.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
        (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b) :
      (i :
          Fin
            (Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a
                  b)).length) →
        Composition
          ((Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a
                  b)).blocksFun
            i))
    (β :=
    (i :
        Fin
          (Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
              (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a
                b')).length) →
      Composition
        ((Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
              (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a
                b')).blocksFun
          i))
    (Sigma.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
        (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a b') :
      (i :
          Fin
            (Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a
                  b')).length) →
        Composition
          ((Sigma.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i))
                (Sigma.mk (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) a
                  b')).blocksFun
            i))
have snd : ∀ (H : Eq (α := Fin a.length → List ℕ) (fun (i : Fin a.length) ↦ (b i).blocks) fun (i : Fin a.length) ↦ (b' i).blocks),
  b = b'
Tactic: simp only [heq_eq_eq, ofFn_inj] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : Eq (α := Fin a.length → List ℕ) (fun (i : Fin a.length) ↦ (b i).blocks) fun (i : Fin a.length) ↦ (b' i).blocks
⊢ b = b'
have snd : ∀ (i : Fin a.length), b i = b' i
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : Eq (α := Fin a.length → List ℕ) (fun (i : Fin a.length) ↦ (b i).blocks) fun (i : Fin a.length) ↦ (b' i).blocks
i : Fin a.length
⊢ b i = b' i
have snd : (b i).blocks = (b' i).blocks
Tactic: ext1
-- 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
H : Type u_5
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
⊢ ∀ {i : ℕ}, i ∈ List.map sum (a.blocks.splitWrtComposition b) → 0 < i
have rw : ∀ j ∈ a.blocks.splitWrtComposition b, 0 < j.sum
Tactic: rw [forall_mem_map]
-- 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
H : Type u_5
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
j : List ℕ
hj : j ∈ a.blocks.splitWrtComposition b
⊢ 0 < j.sum
have suffices : ∀ i ∈ j, 1 ≤ i
Tactic: suffices H : ∀ i ∈ j, 1 ≤ i from calc
      0 < j.length := length_pos_of_mem_splitWrtComposition hj
      _ ≤ j.sum := length_le_sum_of_one_le _ H
-- 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
H : Type u_5
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
j : List ℕ
hj : j ∈ a.blocks.splitWrtComposition b
i : ℕ
hi : i ∈ j
⊢ 1 ≤ i
have apply : i ∈ a.blocks
Tactic: apply a.one_le_blocks
-- 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
H : Type u_5
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
j : List ℕ
hj : j ∈ a.blocks.splitWrtComposition b
i : ℕ
hi : i ∈ j
⊢ i ∈ a.blocks
have rw : i ∈ (a.blocks.splitWrtComposition b).flatten
Tactic: rw [← a.blocks.flatten_splitWrtComposition b]
-- 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
H : Type u_5
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
⊢ (List.map sum (a.blocks.splitWrtComposition b)).sum = n
have rw : (a.blocks.splitWrtComposition b).flatten.sum = n
Tactic: rw [← sum_flatten, flatten_splitWrtComposition, a.blocks_sum]
-- 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
H : Type u_5
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
rw : (a.blocks.splitWrtComposition b).flatten.sum = n
⊢ (List.map sum (a.blocks.splitWrtComposition b)).sum = n
have rw₁ : a.blocks.sum = n
Tactic: rw [← sum_flatten, flatten_splitWrtComposition, a.blocks_sum]
-- 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
H : Type u_5
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
rw : (a.blocks.splitWrtComposition b).flatten.sum = n
rw₁ : a.blocks.sum = n
⊢ (List.map sum (a.blocks.splitWrtComposition b)).sum = n
have rw₂ : n = n
Tactic: rw [← sum_flatten, flatten_splitWrtComposition, a.blocks_sum]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : Composition a.length
⊢ (List.map sum (a.blocks.splitWrtComposition b)).length = b.blocks.length
have rw : (a.blocks.splitWrtComposition b).length = b.blocks.length
Tactic: rw [length_map, length_splitWrtComposition]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : Composition a.length
rw : (a.blocks.splitWrtComposition b).length = b.blocks.length
⊢ (List.map sum (a.blocks.splitWrtComposition b)).length = b.blocks.length
have rw₁ : b.length = b.blocks.length
Tactic: rw [length_map, length_splitWrtComposition]
-- 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
H : Type u_5
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
i : Fin (a.gather b).length
⊢ (↑i : ℕ) < (a.blocks.splitWrtComposition b).length
have rw : (↑i : ℕ) < (a.gather b).length
Tactic: rw [length_splitWrtComposition, ← length_gather]
-- 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
H : Type u_5
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
n : ℕ
a : Composition n
b : Composition a.length
i_1 : Fin (a.gather b).length
i : ℕ
hi :
  i ∈ getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) (↑i_1 : ℕ) ⋯
⊢ i ∈ a.blocks
have rw : i ∈ (a.blocks.splitWrtComposition b).flatten
Tactic: rw [← a.blocks.flatten_splitWrtComposition b]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
⊢ (getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) (↑i : ℕ)
        ⋯).length =
    b.blocksFun i
have rw : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.map List.length (a.blocks.splitWrtComposition b))
    (↑i : ℕ) sorry =
  b.blocksFun i
Tactic: rw [getElem_map_rev List.length, getElem_of_eq (map_length_splitWrtComposition _ _), blocksFun,
      get_eq_getElem]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
rw :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.map List.length (a.blocks.splitWrtComposition b))
      (↑i : ℕ) ⋯ =
    b.blocksFun i
⊢ (getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) (↑i : ℕ)
        ⋯).length =
    b.blocksFun i
have rw₁ : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) sorry = b.blocksFun i
Tactic: rw [getElem_map_rev List.length, getElem_of_eq (map_length_splitWrtComposition _ _), blocksFun,
      get_eq_getElem]