awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N n : ℕ
f : Fin n → ℕ
hi : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f ∈ compPartialSumSource m M N
j : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f))
⊢ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (ofFn (n := n) fun (a : Fin n) ↦ f a) (↑j : ℕ) ⋯ = f j

Tactic:
simp only [List.getElem_ofFn]

Premises used: List.getElem_ofFn
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N : ℕ
i : (n : ℕ) × Composition n
hi : i ∈ compPartialSumTargetSet m M N
rcases :
  ∀ (n : ℕ) (c : Composition n) (hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N),
    ∃ (j : (n : ℕ) × (Fin n → ℕ)) (hj : j ∈ compPartialSumSource m M N),
      compChangeOfVariables m M N j hj = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c
⊢ ∃ (j : (n : ℕ) × (Fin n → ℕ)) (hj : j ∈ compPartialSumSource m M N), compChangeOfVariables m M N j hj = i

Tactic:
rcases i with ⟨n, c⟩
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
⊢ ∃ (j : (n : ℕ) × (Fin n → ℕ)) (hj : j ∈ compPartialSumSource m M N),
    compChangeOfVariables m M N j hj = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c

Tactic:
⟨⟨c.length, c.blocksFun⟩, ?_, ?_⟩

Premises used: Composition.length, Composition.blocksFun, Exists.intro, Sigma.mk
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
refine_1 : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) c.length c.blocksFun ∈ compPartialSumSource m M N
refine_2 :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) c.length c.blocksFun) ⋯ =
    Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c
⊢ ∃ (j : (n : ℕ) × (Fin n → ℕ)) (hj : j ∈ compPartialSumSource m M N),
    compChangeOfVariables m M N j hj = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c

Tactic:
refine ⟨⟨c.length, c.blocksFun⟩, ?_, ?_⟩
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N n : ℕ
c : Composition n
hi : m ≤ c.length ∧ c.length < M ∧ ∀ (j : Fin c.length), c.blocksFun j < N
refine_1 : ∀ (a : Fin c.length), 1 ≤ c.blocksFun a
⊢ Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) c.length c.blocksFun ∈ compPartialSumSource m M N

Tactic:
simp only [mem_compPartialSumSource_iff, hi.left, hi.right, true_and, and_true]

Premises used: and_true, And.right, And.left, true_and, FormalMultilinearSeries.mem_compPartialSumSource_iff
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N n : ℕ
c : Composition n
hi : m ≤ c.length ∧ c.length < M ∧ ∀ (j : Fin c.length), c.blocksFun j < N
⊢ ∀ (a : Fin c.length), 1 ≤ c.blocksFun a

Tactic:
fun a => c.one_le_blocks' _

Premises used: Composition.blocksFun, Fin.isLt, Composition.one_le_blocks'
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N n : ℕ
c : Composition n
hi : m ≤ c.length ∧ c.length < M ∧ ∀ (j : Fin c.length), c.blocksFun j < N
⊢ ∀ (a : Fin c.length), 1 ≤ c.blocksFun a

Tactic:
exact fun a => c.one_le_blocks' _

Premises used: Composition.one_le_blocks'
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
refine_2 :
  (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) (∑ j : Fin c.length, c.blocksFun j)
            { blocks := ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocksFun a, blocks_pos := ⋯, blocks_sum := ⋯ :
              Composition (∑ j : Fin c.length, c.blocksFun j) }).snd
        (β := fun (n : ℕ) ↦ Composition n).blocks =
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks
⊢ Sigma.mk (β := fun (n : ℕ) ↦ Composition n) (∑ j : Fin c.length, c.blocksFun j)
      { blocks := ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocksFun a, blocks_pos := ⋯, blocks_sum := ⋯ :
        Composition (∑ j : Fin c.length, c.blocksFun j) } =
    Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c

Tactic:
rw [Composition.sigma_eq_iff_blocks_eq]

Premises used: Composition.sigma_eq_iff_blocks_eq
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
refine_2 : (ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocks.get a) = c.blocks
⊢ (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) (∑ j : Fin c.length, c.blocksFun j)
            { blocks := ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocksFun a, blocks_pos := ⋯, blocks_sum := ⋯ :
              Composition (∑ j : Fin c.length, c.blocksFun j) }).snd
        (β := fun (n : ℕ) ↦ Composition n).blocks =
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks

Tactic:
simp only [Composition.blocksFun]

Premises used: Composition.blocksFun
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
rw : ofFn c.blocks.get
| c.blocks

Tactic:
rw [← List.ofFn_get c.blocks]

Premises used: List.ofFn_get, Composition.blocks
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
conv_rhs : (ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocks.get a) = c.blocks
refine_2 : (ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocks.get a) = ofFn c.blocks.get
⊢ (ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocks.get a) = c.blocks

Tactic:
conv_rhs => rw [← List.ofFn_get c.blocks]

Premises used: List.ofFn_get, Composition.blocks
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N : ℕ
a : (n : ℕ) × Composition n
⊢ a ∈ compPartialSumTarget m M N ↔
    m ≤ a.snd (β := fun (n : ℕ) ↦ Composition n).length ∧
      a.snd (β := fun (n : ℕ) ↦ Composition n).length < M ∧
        ∀ (j : Fin a.snd (β := fun (n : ℕ) ↦ Composition n).length),
          a.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j < N

Tactic:
simp [compPartialSumTarget, compPartialSumTargetSet]

Premises used: FormalMultilinearSeries.compPartialSumTarget, FormalMultilinearSeries.compPartialSumTargetSet
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
hi :
  ∀ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N),
    compChangeOfVariables m M N a ha ∈ compPartialSumTarget m M N
i_inj :
  ∀ (a₁ : (n : ℕ) × (Fin n → ℕ)) (ha₁ : a₁ ∈ compPartialSumSource m M N) (a₂ : (n : ℕ) × (Fin n → ℕ))
    (ha₂ : a₂ ∈ compPartialSumSource m M N),
    compChangeOfVariables m M N a₁ ha₁ = compChangeOfVariables m M N a₂ ha₂ → a₁ = a₂
i_surj :
  ∀ b ∈ compPartialSumTarget m M N,
    ∃ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N), compChangeOfVariables m M N a ha = b
h₁ : ∀ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N), f a = g (compChangeOfVariables m M N a ha)
⊢ Eq.{u_6 + 1} (α := α) (∑ e ∈ compPartialSumSource m M N, f e) (∑ e ∈ compPartialSumTarget m M N, g e)

Tactic:
apply Finset.sum_bij (compChangeOfVariables m M N)

Premises used: Finset.sum_bij, FormalMultilinearSeries.compChangeOfVariables
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
⊢ (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) ∧
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) < M) ∧
    ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))),
      LE.le (α := ℕ) (1 : ℕ)
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) a : ℕ) ∧
        Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) a < N

Tactic:
rw [mem_compPartialSumSource_iff] at H

Premises used: FormalMultilinearSeries.mem_compPartialSumSource_iff
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H_1 : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
H :
  (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) ∧
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) < M) ∧
    ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))),
      LE.le (α := ℕ) (1 : ℕ)
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) a : ℕ) ∧
        Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) a < N
hi :
  ∀ (j : Fin (length (α := ℕ) (ofFn (n := k) fun (a : Fin k) ↦ blocks_fun a))),
    { blocks := ofFn (n := k) fun (a : Fin k) ↦ blocks_fun a, blocks_pos := ⋯, blocks_sum := ⋯ :
            Composition (∑ j : Fin k, blocks_fun j) }.blocksFun
        j <
      N
⊢ compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H_1 ∈ compPartialSumTarget m M N

Tactic:
simp only [mem_compPartialSumTarget_iff, Composition.length, H.left,
      length_ofFn, true_and, compChangeOfVariables]

Premises used: Composition.length, List.length_ofFn, And.left, FormalMultilinearSeries.compChangeOfVariables, FormalMultilinearSeries.mem_compPartialSumTarget_iff, true_and
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H_1 : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
H :
  (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) ∧
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) < M) ∧
    ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))),
      LE.le (α := ℕ) (1 : ℕ)
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) a : ℕ) ∧
        Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) a < N
j : Fin (length (α := ℕ) (ofFn (n := k) fun (a : Fin k) ↦ blocks_fun a))
⊢ { blocks := ofFn (n := k) fun (a : Fin k) ↦ blocks_fun a, blocks_pos := ⋯, blocks_sum := ⋯ :
          Composition (∑ j : Fin k, blocks_fun j) }.blocksFun
      j <
    N

Tactic:
simp only [Composition.blocksFun, (H.right _).right, List.get_ofFn]

Premises used: List.get_ofFn, Composition.blocksFun, And.right
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
k' : ℕ
blocks_fun' : Fin k' → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun') H'
⊢ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) =
    (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length

Tactic:
have := (compChangeOfVariables_length m M N H).symm
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
k' : ℕ
blocks_fun' : Fin k' → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun') H'
this :
  Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) =
    (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length
rwa :
  ∀
    (this :
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) =
        (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun') H').snd (β :=
            fun (n : ℕ) ↦ Composition n).length),
    k = k'
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (this :
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) =
        Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun')),
    k = k'
⊢ k = k'

Tactic:
rwa [heq, compChangeOfVariables_length] at this

Premises used: FormalMultilinearSeries.compChangeOfVariables_length
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
k' : ℕ
blocks_fun' : Fin k' → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun') H'
i_inj :
  ∀ (blocks_fun' : Fin k → ℕ) (H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun' ∈ compPartialSumSource m M N)
    (heq :
      compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
        compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H'),
    Eq (α := (n : ℕ) × (Fin n → ℕ)) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
      (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun')
⊢ Eq (α := (n : ℕ) × (Fin n → ℕ)) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
    (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun')

Tactic:
obtain rfl : k = k' := by
      have := (compChangeOfVariables_length m M N H).symm
      rwa [heq, compChangeOfVariables_length] at this

Premises used: rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H'
i_inj : blocks_fun = blocks_fun'
⊢ Eq (α := (n : ℕ) × (Fin n → ℕ)) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
    (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun')

Tactic:
congr
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H'
i_inj : ∀ (i : Fin k), blocks_fun i = blocks_fun' i
⊢ blocks_fun = blocks_fun'

Tactic:
funext i
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H'
i : Fin k
⊢ blocks_fun i =
    (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
          Composition n).blocksFun
      ⟨(↑i : ℕ), ⋯⟩

Tactic:
(compChangeOfVariables_blocksFun m M N H i).symm

Premises used: FormalMultilinearSeries.compChangeOfVariables_blocksFun, Eq.symm
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H'
i : Fin k
⊢ (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
          Composition n).blocksFun
      (⟨(↑i : ℕ), ⋯⟩ :
        Fin
          (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
              Composition n).length) =
    (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H').snd (β := fun (n : ℕ) ↦
          Composition n).blocksFun
      ⟨(↑i : ℕ), ⋯⟩

Tactic:
grind
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H'
i : Fin k
⊢ (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H').snd (β := fun (n : ℕ) ↦
          Composition n).blocksFun
      (⟨(↑i : ℕ), ⋯⟩ :
        Fin
          (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H').snd (β :=
              fun (n : ℕ) ↦ Composition n).length) =
    blocks_fun' i

Tactic:
compChangeOfVariables_blocksFun m M N H' i

Premises used: FormalMultilinearSeries.compChangeOfVariables_blocksFun
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H'
i : Fin k
blocks_fun₁ :
  (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
          Composition n).blocksFun
      (⟨(↑i : ℕ), ⋯⟩ :
        Fin
          (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
              Composition n).length) =
    (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H').snd (β := fun (n : ℕ) ↦
          Composition n).blocksFun
      ⟨(↑i : ℕ), ⋯⟩
⊢ blocks_fun i = blocks_fun' i

Tactic:
calc
      blocks_fun i = (compChangeOfVariables m M N _ H).2.blocksFun _ :=
        (compChangeOfVariables_blocksFun m M N H i).symm
      _ = (compChangeOfVariables m M N _ H').2.blocksFun _ := by
        grind
      _ = blocks_fun' i := compChangeOfVariables_blocksFun m M N H' i

Premises used: Composition.blocksFun, FormalMultilinearSeries.compChangeOfVariables_blocksFun, FormalMultilinearSeries.compChangeOfVariables, Eq.symm, Sigma.snd
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
i : (n : ℕ) × Composition n
hi : i ∈ compPartialSumTarget m M N
i_surj : i ∈ compPartialSumTargetSet m M N
⊢ ∃ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N), compChangeOfVariables m M N a ha = i

Tactic:
apply compPartialSumTargetSet_image_compPartialSumSource m M N i

Premises used: FormalMultilinearSeries.compPartialSumTargetSet_image_compPartialSumSource
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
i : (n : ℕ) × Composition n
hi : i ∈ compPartialSumTarget m M N
⊢ i ∈ compPartialSumTargetSet m M N

Tactic:
simpa [compPartialSumTarget] using hi

Premises used: FormalMultilinearSeries.compPartialSumTarget
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
⊢ ∀ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N), f a = g (compChangeOfVariables m M N a ha)

Tactic:
assumption