awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
rw rw₁ :
  Eq (α := FormalMultilinearSeries 𝕜 F E)
    ((p.leftInv i x).comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0)) : FormalMultilinearSeries 𝕜 F E)
    ((p.leftInv i x).comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0)) : FormalMultilinearSeries 𝕜 F E)
⊢ Eq (α := FormalMultilinearSeries 𝕜 F E)
    ((p.leftInv i x).comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0)) : FormalMultilinearSeries 𝕜 F E)
    ((p.leftInv i x).comp (p.comp (p.rightInv i x)) : FormalMultilinearSeries 𝕜 F E)

Tactic:
rw [comp_rightInv p i _ h]

Premises used: FormalMultilinearSeries.comp_rightInv
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
rw rw₁ :
  Eq (α := FormalMultilinearSeries 𝕜 F E)
    ((p.leftInv i x).comp (p.comp (p.rightInv i x)) : FormalMultilinearSeries 𝕜 F E)
    ((p.leftInv i x).comp (p.comp (p.rightInv i x)) : FormalMultilinearSeries 𝕜 F E)
⊢ Eq (α := FormalMultilinearSeries 𝕜 F E)
    ((p.leftInv i x).comp (p.comp (p.rightInv i x)) : FormalMultilinearSeries 𝕜 F E)
    (FormalMultilinearSeries.comp ((p.leftInv i x).comp p) (p.rightInv i x) : FormalMultilinearSeries 𝕜 F E)

Tactic:
rw [comp_assoc]

Premises used: FormalMultilinearSeries.comp_assoc
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
rw rw₁ :
  Eq (α := FormalMultilinearSeries 𝕜 F E)
    (FormalMultilinearSeries.comp (id 𝕜 E x) (p.rightInv i x) : FormalMultilinearSeries 𝕜 F E)
    (FormalMultilinearSeries.comp (id 𝕜 E x) (p.rightInv i x) : FormalMultilinearSeries 𝕜 F E)
⊢ Eq (α := FormalMultilinearSeries 𝕜 F E)
    (FormalMultilinearSeries.comp ((p.leftInv i x).comp p) (p.rightInv i x) : FormalMultilinearSeries 𝕜 F E)
    (FormalMultilinearSeries.comp (id 𝕜 E x) (p.rightInv i x) : FormalMultilinearSeries 𝕜 F E)

Tactic:
rw [leftInv_comp p i _ h]

Premises used: FormalMultilinearSeries.leftInv_comp
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
⊢ FormalMultilinearSeries.comp (id 𝕜 E x) (p.rightInv i x) = p.rightInv i x

Tactic:
simp [id_comp' _ _ 0]

Premises used: FormalMultilinearSeries.id_comp', OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
simp_rw :
  Eq (α := ℝ)
    (∑ x ∈ Ico 2 (n + 1),
      ∑ i ∈ Set.toFinset {c : Composition x | 1 < c.length},
        a ^ x * (r ^ i.length * ∏ j : Fin i.length, p (i.blocksFun j)))
    (∑ k ∈ Ico 2 (n + 1),
      ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
        ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j)))
⊢ Eq (α := ℝ)
    (∑ k ∈ Ico 2 (n + 1),
      a ^ k *
        ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length}, r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j))
    (∑ k ∈ Ico 2 (n + 1),
      ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
        ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j)))

Tactic:
simp_rw [mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
a₁ :
  ∀ k ∈ Ico 2 (n + 1),
    ∀ (c : Composition k),
      Membership.mem (γ := Finset (Composition k)) (Set.toFinset {c : Composition k | 1 < c.length}) c →
        a ^ k * (r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j)) =
          ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j))
⊢ Eq (α := ℝ)
    (∑ x ∈ Ico 2 (n + 1),
      ∑ i ∈ Set.toFinset {c : Composition x | 1 < c.length},
        a ^ x * (r ^ i.length * ∏ j : Fin i.length, p (i.blocksFun j)))
    (∑ k ∈ Ico 2 (n + 1),
      ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
        ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j)))

Tactic:
congr! with k _ c
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
h : k ∈ Ico 2 (n + 1)
c : Composition k
h_1 : Membership.mem (γ := Finset (Composition k)) (Set.toFinset {c : Composition k | 1 < c.length}) c
a₁ :
  a ^ k * (r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j)) =
    r ^ c.length * (a ^ k * ∏ x : Fin c.length, p (c.blocksFun x))
⊢ a ^ k * (r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j)) =
    ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j))

Tactic:
rw [prod_mul_distrib, prod_mul_distrib, prod_pow_eq_pow_sum, Composition.sum_blocksFun,
        prod_const, card_fin]

Premises used: Finset.prod_mul_distrib, Composition.sum_blocksFun, Finset.prod_const, Finset.prod_pow_eq_pow_sum, Finset.card_fin
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
h : k ∈ Ico 2 (n + 1)
c : Composition k
h_1 : Membership.mem (γ := Finset (Composition k)) (Set.toFinset {c : Composition k | 1 < c.length}) c
⊢ a ^ k * (r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j)) =
    r ^ c.length * (a ^ k * ∏ x : Fin c.length, p (c.blocksFun x))

Tactic:
ring
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
rw :
  LE.le (α := ℝ)
    (∑ x ∈ (Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length},
      ∏ j : Fin x.snd.length,
        r *
          (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
            p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j)))
    (∑ d ∈ compPartialSumTarget 2 (n + 1) n,
      ∏ j : Fin d.snd.length,
        r *
          (a ^ d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j *
            p (d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j)))
⊢ LE.le (α := ℝ)
    (∑ k ∈ Ico 2 (n + 1),
      ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
        ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j)))
    (∑ d ∈ compPartialSumTarget 2 (n + 1) n,
      ∏ j : Fin d.snd.length,
        r *
          (a ^ d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j *
            p (d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j)))

Tactic:
rw [sum_sigma']

Premises used: Finset.sum_sigma'
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hf :
  ∀ i ∈ compPartialSumTarget 2 (n + 1) n,
    (i ∉ (Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length}) →
      LE.le (α := ℝ) 0
        (∏ j : Fin i.snd.length,
          r *
            (a ^ i.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
              p (i.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j)))
h :
  ((Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length}) ⊆
    compPartialSumTarget 2 (n + 1) n
⊢ LE.le (α := ℝ)
    (∑ x ∈ (Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length},
      ∏ j : Fin x.snd.length,
        r *
          (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
            p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j)))
    (∑ d ∈ compPartialSumTarget 2 (n + 1) n,
      ∏ j : Fin d.snd.length,
        r *
          (a ^ d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j *
            p (d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j)))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
x : (i : ℕ) × Composition i
hf :
  x ∈ compPartialSumTarget 2 (n + 1) n →
    (x ∉ (Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length}) →
      LE.le (α := ℝ) 0
        (∏ j : Fin x.snd.length,
          r *
            (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
              p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j)))
⊢ x ∈ compPartialSumTarget 2 (n + 1) n →
    (x ∉ (Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length}) →
      LE.le (α := ℝ) 0
        (∏ j : Fin x.snd.length,
          r *
            (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
              p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j)))

Tactic:
_
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
x : (i : ℕ) × Composition i
h : x ∈ compPartialSumTarget 2 (n + 1) n
hf :
  (x ∉ (Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length}) →
    LE.le (α := ℝ) 0
      (∏ j : Fin x.snd.length,
        r *
          (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
            p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j)))
⊢ (x ∉ (Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length}) →
    LE.le (α := ℝ) 0
      (∏ j : Fin x.snd.length,
        r *
          (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
            p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j)))

Tactic:
_
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
x : (i : ℕ) × Composition i
h : x ∈ compPartialSumTarget 2 (n + 1) n
h_1 : x ∉ (Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length}
j : Fin x.snd (β := fun (i : ℕ) ↦ Composition i).length
h_2 : Membership.mem (γ := Finset (Fin x.snd (β := fun (i : ℕ) ↦ Composition i).length)) univ j
positivity positivity₁ positivity₂ :
  0 ≤ a →
    0 ≤
      r *
        (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
          p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j))
positivity₃ positivity₄ :
  0 ≤ a →
    0 ≤ p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j) →
      0 ≤
        r *
          (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
            p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j))
⊢ 0 ≤
    r *
      (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
        p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j))

Tactic:
positivity [ha, hp (x.snd.blocksFun j)]

Premises used: Composition.blocksFun, Sigma.snd
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
x : (i : ℕ) × Composition i
h : x ∈ compPartialSumTarget 2 (n + 1) n
h_1 : x ∉ (Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length}
⊢ LE.le (α := ℝ) 0
    (∏ j : Fin x.snd.length,
      r *
        (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
          p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j)))

Tactic:
exact prod_nonneg fun j _ ↦ (by positivity [ha, hp (x.snd.blocksFun j)])

Premises used: Finset.prod_nonneg
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd :
  Membership.mem (γ := Finset ((i : ℕ) × Composition i))
    ((Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length})
    (Sigma.mk (β := fun (i : ℕ) ↦ Composition i) k c)
⊢ (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length

Tactic:
simp only [Set.mem_toFinset (s := {c | 1 < Composition.length c}), mem_Ico, mem_sigma,
        Set.mem_setOf_eq] at hd

Premises used: Finset.mem_sigma, Set.mem_setOf_eq, Set.mem_toFinset, Finset.mem_Ico
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
h : 2 ≤ c.length ∧ c.length < n + 1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n
⊢ Sigma.mk (β := fun (i : ℕ) ↦ Composition i) k c ∈ compPartialSumTarget 2 (n + 1) n

Tactic:
simp only [mem_compPartialSumTarget_iff]

Premises used: FormalMultilinearSeries.mem_compPartialSumTarget_iff
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
⊢ 2 ≤ c.length ∧ c.length < n + 1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n

Tactic:
⟨hd.2, c.length_le.trans_lt hd.1.2, fun j => ?_⟩

Premises used: And.right, And.left, Composition.length_le, And.intro, LE.le.trans_lt
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
h : ∀ (j : Fin c.length), c.blocksFun j < n
⊢ 2 ≤ c.length ∧ c.length < n + 1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n

Tactic:
refine ⟨hd.2, c.length_le.trans_lt hd.1.2, fun j => ?_⟩
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
j : Fin c.length
⊢ c ≠ Composition.single k ⋯

Tactic:
simp [Composition.eq_single_iff_length, ne_of_gt hd.2]

Premises used: ne_of_gt, And.right, Composition.eq_single_iff_length
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
j : Fin c.length
⊢ c ≠ Composition.single k ⋯

Tactic:
have : c ≠ Composition.single k (zero_lt_two.trans_le hd.1.1) := by
        simp [Composition.eq_single_iff_length, ne_of_gt hd.2]
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
j : Fin c.length
this : c ≠ Composition.single k ⋯
⊢ ∀ (i : Fin c.length), c.blocksFun i < k

Tactic:
rw [Composition.ne_single_iff] at this

Premises used: Composition.ne_single_iff
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
j : Fin c.length
this : ∀ (i : Fin c.length), c.blocksFun i < k
⊢ c.blocksFun j < n

Tactic:
(this j).trans_le (Nat.lt_succ_iff.mp hd.1.2)

Premises used: And.right, Nat.lt_succ_iff, And.left, LT.lt.trans_le, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
j : Fin c.length
this : ∀ (i : Fin c.length), c.blocksFun i < k
⊢ c.blocksFun j < n

Tactic:
exact (this j).trans_le (Nat.lt_succ_iff.mp hd.1.2)

Premises used: And.right, Nat.lt_succ_iff, And.left, LT.lt.trans_le, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
symm :
  Eq (α := ℝ)
    (∑ e ∈ compPartialSumSource 2 (n + 1) n,
      ∏ j : Fin e.fst, r * (a ^ e.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) j * p (e.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) j)))
    (∑ d ∈ compPartialSumTarget 2 (n + 1) n,
      ∏ j : Fin d.snd.length,
        r *
          (a ^ d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j *
            p (d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j)))
⊢ Eq (α := ℝ)
    (∑ d ∈ compPartialSumTarget 2 (n + 1) n,
      ∏ j : Fin d.snd.length,
        r *
          (a ^ d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j *
            p (d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j)))
    (∑ e ∈ compPartialSumSource 2 (n + 1) n,
      ∏ j : Fin e.fst, r * (a ^ e.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) j * p (e.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) j)))

Tactic:
symm
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
h :
  ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource 2 (n + 1) n),
    Eq (α := ℝ)
      (∏ j : Fin e.fst, r * (a ^ e.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) j * p (e.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) j)))
      (∏ j : Fin (compChangeOfVariables 2 (n + 1) n e he).snd.length,
        r *
          (a ^ (compChangeOfVariables 2 (n + 1) n e he).snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j *
            p ((compChangeOfVariables 2 (n + 1) n e he).snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j)))
⊢ Eq (α := ℝ)
    (∑ e ∈ compPartialSumSource 2 (n + 1) n,
      ∏ j : Fin e.fst, r * (a ^ e.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) j * p (e.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) j)))
    (∑ d ∈ compPartialSumTarget 2 (n + 1) n,
      ∏ j : Fin d.snd.length,
        r *
          (a ^ d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j *
            p (d.snd (β := fun (n : ℕ) ↦ Composition n).blocksFun j)))

Tactic:
apply compChangeOfVariables_sum

Premises used: FormalMultilinearSeries.compChangeOfVariables_sum
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun ∈ compPartialSumSource 2 (n + 1) n
⊢ (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    k

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun ∈ compPartialSumSource 2 (n + 1) n
⊢ (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    k

Tactic:
have K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length = k := by simp
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun ∈ compPartialSumSource 2 (n + 1) n
K :
  (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    k
h h₁ : Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) = k
⊢ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) =
    (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length

Tactic:
rw [K]
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun ∈ compPartialSumSource 2 (n + 1) n
K :
  (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    k
h h₁ : Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) = k
⊢ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) =
    (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length

Tactic:
try rw [K]
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun ∈ compPartialSumSource 2 (n + 1) n
K :
  (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    k
h h₁ : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun)) = Fin k
⊢ Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun)) =
    Fin
      (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
          fun (n : ℕ) ↦ Composition n).length

Tactic:
rw [K]
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun ∈ compPartialSumSource 2 (n + 1) n
K :
  (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    k
h h₁ : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun)) = Fin k
⊢ Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun)) =
    Fin
      (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
          fun (n : ℕ) ↦ Composition n).length

Tactic:
try rw [K]
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun ∈ compPartialSumSource 2 (n + 1) n
K :
  (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    k
h h₁ :
  HEq (α :=
    Fintype (Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun))))
    (Fin.fintype (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun)))
    (Fin.fintype k)
⊢ HEq (α :=
    Fintype (Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun))))
    (Fin.fintype (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun))) (β :=
    Fintype
      (Fin
        (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
            fun (n : ℕ) ↦ Composition n).length))
    (Fin.fintype
      (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
          fun (n : ℕ) ↦ Composition n).length)

Tactic:
rw [K]