awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
j : (a : Composition n) × Composition a.length
a : Composition n
b : Composition a.length
rcases :
  ∀ (a' : Composition n) (b' : Composition a'.length),
    (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
              (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
          (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
              (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')).blocks ∧
        blocks (n :=
            (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
                (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
            (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
              (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
          blocks (n :=
            (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
                (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')).length)
            (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
              (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')) →
      Eq (α := (a : Composition n) × Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')
⊢ (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
        j.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks ∧
      blocks (n :=
          (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
              (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
          (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
        j.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks →
    Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b = j

Tactic:
rcases j with ⟨a', b'⟩
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h :
  (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
    (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')).blocks
h' :
  Composition.blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
    Composition.blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b'))
blocks : a.blocks = a'.blocks
⊢ a = a'

Tactic:
ext1
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h :
  (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
    (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')).blocks
h' :
  blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
    blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b'))
⊢ a.blocks = a'.blocks

Tactic:
h
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h :
  (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
    (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')).blocks
h' :
  blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
    blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b'))
⊢ a.blocks = a'.blocks

Tactic:
exact h
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h :
  (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
    (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')).blocks
h' :
  blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
    blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b'))
obtain :
  ∀ (b' : Composition a.length)
    (h :
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
        (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')).blocks)
    (h' :
      blocks (n :=
          (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
              (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
          (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
        blocks (n :=
          (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
              (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')).length)
          (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b'))),
    Eq (α := (a : Composition n) × Composition a.length)
      (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)
      (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')
⊢ Eq (α := (a : Composition n) × Composition a.length)
    (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)
    (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a' b')

Tactic:
obtain rfl : a = a' := by ext1; exact h

Premises used: rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b b' : Composition a.length
h :
  (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
    (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')).blocks
h' :
  Composition.blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
    Composition.blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b'))
blocks : b.blocks = b'.blocks
⊢ b = b'

Tactic:
ext1
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b b' : Composition a.length
h :
  (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
    (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')).blocks
h' :
  blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
    blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b'))
⊢ b.blocks = b'.blocks

Tactic:
h'
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b b' : Composition a.length
h :
  (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
    (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')).blocks
h' :
  blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
    blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b'))
⊢ b.blocks = b'.blocks

Tactic:
exact h'
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b b' : Composition a.length
h :
  (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
    (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')).blocks
h' :
  blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
    blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b'))
obtain :
  ∀
    (h :
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
        (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks)
    (h' :
      blocks (n :=
          (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
              (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
          (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
        blocks (n :=
          (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
              (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
          (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
            (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b))),
    Eq (α := (a : Composition n) × Composition a.length)
      (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)
      (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)
⊢ Eq (α := (a : Composition n) × Composition a.length)
    (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)
    (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b')

Tactic:
obtain rfl : b = b' := by ext1; exact h'

Premises used: rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
a : Composition n
b : Composition a.length
h :
  (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
    (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks
h' :
  blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
    blocks (n :=
      (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
          (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
      (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
        (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b))
⊢ Eq (α := (a : Composition n) × Composition a.length)
    (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)
    (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)

Tactic:
rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
H : u = v
rw 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)
⊢ 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)

Tactic:
rw [H]
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
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
⊢ 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)

Tactic:
refine ⟨fun H => by rw [H], fun H => ?_⟩
-- Module: Mathlib.Analysis.Analytic.Composition
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)
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
⊢ u = v

Tactic:
rcases u with ⟨a, b⟩
-- 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)
blocks : a.blocks = a'.blocks
⊢ a = a'

Tactic:
ext1
-- 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)
rw 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))
⊢ 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]
-- 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)
⊢ 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]
-- 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 ℕ) (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))
⊢ 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

Premises used: List.map_ofFn