awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
i j : ℕ
hi : i < b.length
hj : j < b.blocksFun ⟨i, hi⟩
zero :
  ∀ (hj : 0 < b.blocksFun (⟨i, hi⟩ : Fin b.length)),
    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
succ :
  ∀ (j : ℕ)
    (IHj :
      ∀ (hj : j < b.blocksFun ⟨i, hi⟩),
        a.sizeUpTo (b.sizeUpTo i + j) =
          (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)) j)
    (hj : j + 1 < b.blocksFun ⟨i, hi⟩),
    a.sizeUpTo (b.sizeUpTo i + (j + 1)) =
      (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)) (j + 1)
⊢ a.sizeUpTo (b.sizeUpTo i + j) =
    (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)) j

Tactic:
induction j with
  | zero =>
    change
      sum (take (b.blocks.take i).sum a.blocks) =
        sum (take i (map sum (splitWrtComposition a.blocks b)))
    induction i with
    | zero => rfl
    | succ i IH =>
      have A : i < b.length := Nat.lt_of_succ_lt hi
      have B : i < List.length (map List.sum (splitWrtComposition a.blocks b)) := by simp [A]
      have C : 0 < blocksFun b ⟨i, A⟩ := Composition.blocks_pos' _ _ _
      rw [sum_take_succ _ _ B, ← IH A C]
      have :
        take (sum (take i b.blocks)) a.blocks =
          take (sum (take i b.blocks)) (take (sum (take (i + 1) b.blocks)) a.blocks) := by
        rw [take_take, min_eq_left]
        apply monotone_sum_take _ (Nat.le_succ _)
      rw [this, getElem_map, getElem_splitWrtComposition, ←
        take_append_drop (sum (take i b.blocks)) (take (sum (take (Nat.succ i) b.blocks)) a.blocks),
        sum_append]
      congr
      rw [take_append_drop]
  | succ j IHj =>
    have A : j < blocksFun b ⟨i, hi⟩ := lt_trans (lt_add_one j) hj
    have B : j < length (sigmaCompositionAux a b ⟨i, (length_gather a b).symm ▸ hi⟩) := by
      convert! A; rw [← length_sigmaCompositionAux]
    have C : sizeUpTo b i + j < sizeUpTo b (i + 1) := by
      simp only [sizeUpTo_succ b hi, add_lt_add_iff_left]
      exact A
    have D : sizeUpTo b i + j < length a := lt_of_lt_of_le C (b.sizeUpTo_le _)
    have : sizeUpTo b i + Nat.succ j = (sizeUpTo b i + j).succ := rfl
    rw [this, sizeUpTo_succ _ D, IHj A, sizeUpTo_succ _ B]
    simp only [sigmaCompositionAux, add_assoc]
    rw [getElem_of_eq (getElem_splitWrtComposition _ _ _ _), getElem_drop, getElem_take]

Premises used: List.map, add_assoc, Composition.blocks, List.sum, List.take_append_drop, List.getElem_of_eq, List.getElem_take, List.getElem_drop, List.splitWrtComposition, List.getElem_map, List.sum_append, Composition.sigmaCompositionAux, Nat.succ, List.take, List.getElem_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_1 n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
simp :
  ∀ {i_1 : ℕ} (j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length),
    i_1 ∈ (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks → 0 < i_1
⊢ ∀ {i_1 : ℕ},
    Membership.mem (γ := List ℕ)
        (flatten
          (ofFn (n := i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
            fun
              (j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
            (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks))
        i_1 →
      0 < i_1

Tactic:
simp only [and_imp, List.mem_flatten, exists_imp, forall_mem_ofFn_iff]

Premises used: and_imp, List.forall_mem_ofFn_iff, List.mem_flatten, exists_imp
-- 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_1 n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
⊢ ∀ {i_1 : ℕ} (j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length),
    i_1 ∈ (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks → 0 < i_1

Tactic:
fun {i} j hj => Composition.blocks_pos _ hj

Premises used: Composition.blocks_pos, Sigma.snd
-- 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_1 n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
⊢ ∀ {i_1 : ℕ} (j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length),
    i_1 ∈ (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks → 0 < i_1

Tactic:
exact fun {i} j hj => Composition.blocks_pos _ hj

Premises used: Composition.blocks_pos
-- 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_1 n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
⊢ sum
      (flatten
        (ofFn (n := i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
          fun (j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
          (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks)) =
    n

Tactic:
simp [sum_ofFn, Composition.blocks_sum, Composition.sum_blocksFun]

Premises used: Composition.sum_blocksFun, List.sum_ofFn, Composition.blocks_sum
-- 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_1 n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
k : ℕ
hk :
  Membership.mem (γ := List ℕ)
    (ofFn (n := i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
      fun (j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).length)
    k
⊢ 0 < k

Tactic:
((forall_mem_ofFn_iff (P := fun i => 0 < i)).2 fun j => ?_) k hk

Premises used: Iff.mpr, List.forall_mem_ofFn_iff
-- 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_1 n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
k : ℕ
hk :
  Membership.mem (γ := List ℕ)
    (ofFn (n := i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
      fun (j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).length)
    k
refine :
  ∀ (j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length),
    0 < (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).length
⊢ 0 < k

Tactic:
refine ((forall_mem_ofFn_iff (P := fun i => 0 < i)).2 fun j => ?_) k hk

Premises used: Iff.mpr, List.forall_mem_ofFn_iff
-- 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_1 n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
k : ℕ
hk :
  Membership.mem (γ := List ℕ)
    (ofFn (n := i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
      fun (j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).length)
    k
j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length
⊢ 0 < (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).length

Tactic:
Composition.length_pos_of_pos _ (Composition.blocks_pos' _ _ _)

Premises used: Composition.blocks_pos', Composition.length_pos_of_pos
-- 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_1 n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
k : ℕ
hk :
  Membership.mem (γ := List ℕ)
    (ofFn (n := i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
      fun (j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
      (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).length)
    k
j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length
⊢ 0 < (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).length

Tactic:
exact Composition.length_pos_of_pos _ (Composition.blocks_pos' _ _ _)

Premises used: Composition.blocks_pos', Composition.length_pos_of_pos
-- 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_1 n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
dsimp :
  sum
      (ofFn (n :=
        i.fst (β := fun (c : Composition n) ↦ (i : Fin c.blocks.length) → Composition (c.blocksFun i)).blocks.length)
        fun
          (j :
            Fin
              i.fst (β := fun (c : Composition n) ↦
                    (i : Fin c.blocks.length) → Composition (c.blocksFun i)).blocks.length) ↦
        (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.blocks.length) → Composition (c.blocksFun i))
              j).blocks.length) =
    List.length (α := ℕ)
      (flatten
        (ofFn (n :=
          i.fst (β := fun (c : Composition n) ↦ (i : Fin c.blocks.length) → Composition (c.blocksFun i)).blocks.length)
          fun
            (j :
              Fin
                i.fst (β := fun (c : Composition n) ↦
                      (i : Fin c.blocks.length) → Composition (c.blocksFun i)).blocks.length) ↦
          (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.blocks.length) → Composition (c.blocksFun i)) j).blocks))
⊢ sum
      (ofFn (n := i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
        fun (j : Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
        (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).length) =
    {
        blocks :=
          flatten
            (ofFn (n := i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length)
              fun
                (j :
                  Fin i.fst (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)).length) ↦
              (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.length) → Composition (c.blocksFun i)) j).blocks),
        blocks_pos := ⋯, blocks_sum := ⋯ : Composition n }.length

Tactic:
dsimp only [Composition.length]

Premises used: Composition.length
-- 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_1 n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
⊢ sum
      (ofFn (n :=
        i.fst (β := fun (c : Composition n) ↦ (i : Fin c.blocks.length) → Composition (c.blocksFun i)).blocks.length)
        fun
          (j :
            Fin
              i.fst (β := fun (c : Composition n) ↦
                    (i : Fin c.blocks.length) → Composition (c.blocksFun i)).blocks.length) ↦
        (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.blocks.length) → Composition (c.blocksFun i))
              j).blocks.length) =
    List.length (α := ℕ)
      (flatten
        (ofFn (n :=
          i.fst (β := fun (c : Composition n) ↦ (i : Fin c.blocks.length) → Composition (c.blocksFun i)).blocks.length)
          fun
            (j :
              Fin
                i.fst (β := fun (c : Composition n) ↦
                      (i : Fin c.blocks.length) → Composition (c.blocksFun i)).blocks.length) ↦
          (i.snd (β := fun (c : Composition n) ↦ (i : Fin c.blocks.length) → Composition (c.blocksFun i)) j).blocks))

Tactic:
simp [sum_ofFn]

Premises used: List.sum_ofFn
-- 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_1 n : ℕ
a : Composition n
b : Composition a.length
left :
  flatten (ofFn (n := (a.gather b).length) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).blocks) =
    a.blocks
right :
  (ofFn (n := (a.gather b).length) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).length) = b.blocks
⊢ flatten (ofFn (n := (a.gather b).length) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).blocks) =
      a.blocks ∧
    (ofFn (n := (a.gather b).length) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).length) = b.blocks

Tactic:
constructor
-- 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_1 n : ℕ
a : Composition n
b : Composition a.length
rw : (ofFn (a.blocks.splitWrtComposition b).get).flatten
| a.blocks

Tactic:
rw [← flatten_splitWrtComposition a.blocks b, ← ofFn_get (splitWrtComposition a.blocks b)]

Premises used: List.ofFn_get, Composition.blocks, List.splitWrtComposition, 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_1 n : ℕ
a : Composition n
b : Composition a.length
left :
  flatten (ofFn (n := (a.gather b).length) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).blocks) =
    (ofFn (a.blocks.splitWrtComposition b).get).flatten
⊢ flatten (ofFn (n := (a.gather b).length) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).blocks) =
    a.blocks

Tactic:
conv_rhs =>
        rw [← flatten_splitWrtComposition a.blocks b, ← ofFn_get (splitWrtComposition a.blocks b)]

Premises used: List.ofFn_get, Composition.blocks, List.splitWrtComposition, 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_1 n : ℕ
a : Composition n
b : Composition a.length
⊢ (a.gather b).length = (a.blocks.splitWrtComposition b).length

Tactic:
simp only [length, gather, length_map, length_splitWrtComposition]

Premises used: List.length_splitWrtComposition, Composition.length, List.length_map, Composition.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_1 n : ℕ
a : Composition n
b : Composition a.length
⊢ (a.gather b).length = (a.blocks.splitWrtComposition b).length

Tactic:
have A : length (gather a b) = List.length (splitWrtComposition a.blocks b) := by
        simp only [length, gather, length_map, length_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_1 n : ℕ
a : Composition n
b : Composition a.length
A : (a.gather b).length = (a.blocks.splitWrtComposition b).length
left :
  HEq (α := Fin (a.gather b).length → List ℕ) (fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).blocks)
    (a.blocks.splitWrtComposition b).get
⊢ flatten (ofFn (n := (a.gather b).length) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).blocks) =
    (ofFn (a.blocks.splitWrtComposition b).get).flatten

Tactic:
congr! 2
-- 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_1 n : ℕ
a : Composition n
b : Composition a.length
A : (a.gather b).length = (a.blocks.splitWrtComposition b).length
⊢ HEq (α := Fin (a.gather b).length → List ℕ) (fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).blocks)
    (a.blocks.splitWrtComposition b).get

Tactic:
(Fin.heq_fun_iff A (α := List ℕ)).2 fun i => rfl

Premises used: Iff.mpr, Fin.heq_fun_iff, rfl
-- 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_1 n : ℕ
a : Composition n
b : Composition a.length
A : (a.gather b).length = (a.blocks.splitWrtComposition b).length
⊢ HEq (α := Fin (a.gather b).length → List ℕ) (fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).blocks)
    (a.blocks.splitWrtComposition b).get

Tactic:
exact (Fin.heq_fun_iff A (α := List ℕ)).2 fun i => rfl

Premises used: Iff.mpr, Fin.heq_fun_iff, rfl
-- 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_1 n : ℕ
a : Composition n
b : Composition a.length
⊢ (a.gather b).length = b.blocks.length

Tactic:
have B : Composition.length (Composition.gather a b) = List.length b.blocks :=
        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_1 n : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
rw :
  ofFn (n := b.blocks.length) fun (i : Fin b.blocks.length) ↦
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯
| b.blocks

Tactic:
rw [← ofFn_getElem (xs := b.blocks)]

Premises used: List.ofFn_getElem
-- 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_1 n : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
right :
  Eq (α := List ℕ)
    (ofFn (n := (a.gather b).length) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).length)
    (ofFn (n := b.blocks.length) fun (i : Fin b.blocks.length) ↦
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) b.blocks (↑i : ℕ) ⋯)
⊢ (ofFn (n := (a.gather b).length) fun (j : Fin (a.gather b).length) ↦ (a.sigmaCompositionAux b j).length) = b.blocks

Tactic:
conv_rhs => rw [← ofFn_getElem (xs := b.blocks)]

Premises used: List.ofFn_getElem