awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
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))
⊢ 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

Premises used: Composition.blocks, List.sum, List.ofFn
-- Module: Mathlib.Analysis.Analytic.Composition
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) fun (i : Fin a.length) ↦ (b i).blocks.sum)
    (ofFn (n := a'.length) fun (i : Fin a'.length) ↦ (b' i).blocks.sum)
⊢ a.blocks = a'.blocks

Tactic:
simpa [Composition.blocks_sum, Composition.ofFn_blocksFun] using this

Premises used: Composition.ofFn_blocksFun, Composition.blocks_sum
-- Module: Mathlib.Analysis.Analytic.Composition
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)
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')
⊢ 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

Premises used: rfl
-- Module: Mathlib.Analysis.Analytic.Composition
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)
⊢ 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:
rfl
-- Module: Mathlib.Analysis.Analytic.Composition
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)
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'
⊢ 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))

Tactic:
simp only [heq_eq_eq, ofFn_inj] at H ⊢

Premises used: heq_eq_eq, List.ofFn_inj
-- Module: Mathlib.Analysis.Analytic.Composition
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
snd : ∀ (i : Fin a.length), b i = b' i
⊢ b = b'

Tactic:
ext1 i
-- Module: Mathlib.Analysis.Analytic.Composition
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
snd : (b i).blocks = (b' i).blocks
⊢ b i = b' i

Tactic:
ext1
-- Module: Mathlib.Analysis.Analytic.Composition
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).blocks = (b' i).blocks

Tactic:
congrFun H i

Premises used: congrFun
-- Module: Mathlib.Analysis.Analytic.Composition
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).blocks = (b' i).blocks

Tactic:
exact congrFun H i

Premises used: congrFun
-- 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 : 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 : ∀ j ∈ a.blocks.splitWrtComposition b, 0 < j.sum
⊢ ∀ {i : ℕ}, i ∈ List.map sum (a.blocks.splitWrtComposition b) → 0 < i

Tactic:
rw [forall_mem_map]

Premises used: List.forall_mem_map
-- 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 : 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
suffices : ∀ i ∈ j, 1 ≤ i
⊢ 0 < j.sum

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
-- 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 : 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
apply : i ∈ a.blocks
⊢ 1 ≤ i

Tactic:
apply a.one_le_blocks

Premises used: Composition.one_le_blocks
-- 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 : 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
rw : i ∈ (a.blocks.splitWrtComposition b).flatten
⊢ i ∈ a.blocks

Tactic:
rw [← a.blocks.flatten_splitWrtComposition b]

Premises used: Composition.blocks, List.flatten_splitWrtComposition
-- 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 : 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.splitWrtComposition b).flatten

Tactic:
mem_flatten_of_mem hj hi

Premises used: List.mem_flatten_of_mem
-- 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 : 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.splitWrtComposition b).flatten

Tactic:
exact mem_flatten_of_mem hj hi

Premises used: List.mem_flatten_of_mem
-- 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 : 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
rw₂ rw₃ : n = n
⊢ (List.map sum (a.blocks.splitWrtComposition b)).sum = n

Tactic:
rw [← sum_flatten, flatten_splitWrtComposition, a.blocks_sum]

Premises used: List.sum_flatten, Composition.blocks_sum, List.flatten_splitWrtComposition
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
rw : (a.blocks.splitWrtComposition b).length = b.blocks.length
rw₁ rw₂ : b.length = b.blocks.length
⊢ (List.map sum (a.blocks.splitWrtComposition b)).length = b.blocks.length

Tactic:
rw [length_map, length_splitWrtComposition]

Premises used: List.length_splitWrtComposition, List.length_map
-- 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 : 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
rw : (↑i : ℕ) < (a.gather b).length
⊢ (↑i : ℕ) < (a.blocks.splitWrtComposition b).length

Tactic:
rw [length_splitWrtComposition, ← length_gather]

Premises used: List.length_splitWrtComposition, Composition.length_gather
-- 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 : 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.gather b).length

Tactic:
i.2

Premises used: Fin.isLt
-- 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 : 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.gather b).length

Tactic:
exact i.2

Premises used: Fin.isLt
-- 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 : 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 : ℕ) ⋯
rw : i ∈ (a.blocks.splitWrtComposition b).flatten
⊢ i ∈ a.blocks

Tactic:
rw [← a.blocks.flatten_splitWrtComposition b]

Premises used: Composition.blocks, List.flatten_splitWrtComposition
-- 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 : 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.splitWrtComposition b).flatten

Tactic:
mem_flatten_of_mem (List.getElem_mem _) hi

Premises used: List.getElem_mem, List.mem_flatten_of_mem
-- 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 : 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.splitWrtComposition b).flatten

Tactic:
exact mem_flatten_of_mem (List.getElem_mem _) hi

Premises used: List.getElem_mem, List.mem_flatten_of_mem
-- 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 : 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
⊢ (getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) (↑i : ℕ)
        ⋯).sum =
    (a.gather b).blocksFun i

Tactic:
simp [Composition.blocksFun, getElem_map, Composition.gather]

Premises used: Composition.blocksFun, List.getElem_map, Composition.gather
-- Module: Mathlib.Analysis.Analytic.Composition
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
rw₁ : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯ = b.blocksFun i
rw₂ : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯ = b.blocks.get i
rw₃ rw₄ :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯ =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯
⊢ (getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b) (↑i : ℕ)
        ⋯).length =
    b.blocksFun i

Tactic:
rw [getElem_map_rev List.length, getElem_of_eq (map_length_splitWrtComposition _ _), blocksFun,
      get_eq_getElem]

Premises used: List.get_eq_getElem, Composition.blocksFun, List.getElem_map_rev, List.getElem_of_eq, List.map_length_splitWrtComposition, List.length
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
rw :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) a.blocks
      (b.sizeUpTo (↑(⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length) : ℕ) +
        (↑(⟨(↑j : ℕ), ⋯⟩ :
              Fin
                (length (n := (a.gather b).blocksFun (⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length))
                  {
                    blocks :=
                      getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length)
                        (a.blocks.splitWrtComposition b) (↑(⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length) : ℕ) ⋯,
                    blocks_pos := ⋯, blocks_sum := ⋯ :
                    Composition ((a.gather b).blocksFun (⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length)) })) :
          ℕ))
      ⋯ =
    a.blocksFun ((b.embedding i : (a_1 : Fin (b.blocksFun i)) → Fin a.length) j)
⊢ blocksFun (n := (a.gather b).blocksFun (⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length))
      {
        blocks :=
          getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b)
            (↑(⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length) : ℕ) ⋯,
        blocks_pos := ⋯, blocks_sum := ⋯ :
        Composition ((a.gather b).blocksFun (⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length)) }
      (⟨(↑j : ℕ), ⋯⟩ :
        Fin
          (length (n := (a.gather b).blocksFun (⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length))
            {
              blocks :=
                getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length) (a.blocks.splitWrtComposition b)
                  (↑(⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length) : ℕ) ⋯,
              blocks_pos := ⋯, blocks_sum := ⋯ :
              Composition ((a.gather b).blocksFun (⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length)) })) =
    a.blocksFun ((b.embedding i : (a_1 : Fin (b.blocksFun i)) → Fin a.length) j)

Tactic:
rw [blocksFun, get_eq_getElem, getElem_of_eq (getElem_splitWrtComposition _ _ _ _),
    getElem_drop, getElem_take]

Premises used: List.get_eq_getElem, Composition.blocksFun, List.getElem_of_eq, List.getElem_take, List.getElem_drop, List.getElem_splitWrtComposition
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) a.blocks
      (b.sizeUpTo (↑(⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length) : ℕ) +
        (↑(⟨(↑j : ℕ), ⋯⟩ :
              Fin
                (length (n := (a.gather b).blocksFun (⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length))
                  {
                    blocks :=
                      getElem (valid := fun (as : List (List ℕ)) (i : ℕ) ↦ i < as.length)
                        (a.blocks.splitWrtComposition b) (↑(⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length) : ℕ) ⋯,
                    blocks_pos := ⋯, blocks_sum := ⋯ :
                    Composition ((a.gather b).blocksFun (⟨(↑i : ℕ), ⋯⟩ : Fin (a.gather b).length)) })) :
          ℕ))
      ⋯ =
    a.blocksFun ((b.embedding i : (a_1 : Fin (b.blocksFun i)) → Fin a.length) j)

Tactic:
rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)
zero : (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
⊢ a.sizeUpTo (b.sizeUpTo i + 0) =
    (a.gather b).sizeUpTo i +
      sizeUpTo (n := (a.gather b).blocksFun (⟨i, ⋯⟩ : Fin (a.gather b).length))
        (a.sigmaCompositionAux b (⟨i, ⋯⟩ : Fin (a.gather b).length)) 0

Tactic:
change
      sum (take (b.blocks.take i).sum a.blocks) =
        sum (take i (map sum (splitWrtComposition a.blocks b)))

Premises used: List.map, Composition.blocks, List.sum, List.splitWrtComposition, List.take
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
hi : 0 < b.length
hj : 0 < b.blocksFun (⟨0, hi⟩ : Fin b.length)
⊢ (take (take 0 b.blocks).sum a.blocks).sum = (take 0 (List.map sum (a.blocks.splitWrtComposition b))).sum

Tactic:
rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)
⊢ i < b.length

Tactic:
have A : i < b.length := Nat.lt_of_succ_lt hi
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length) (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun (⟨i + 1, hi⟩ : Fin b.length)
A : i < b.length
⊢ i < (List.map sum (a.blocks.splitWrtComposition b)).length

Tactic:
simp [A]