awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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))
⊢ 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)
have 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)
Tactic: rw [leftInv_comp p i _ h]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ 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)))
have 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)))
Tactic: simp_rw [mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ 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)))
have 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))
Tactic: congr! with k _ c
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)) =
    ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j))
have 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))
Tactic: rw [prod_mul_distrib, prod_mul_distrib, prod_pow_eq_pow_sum, Composition.sum_blocksFun,
        prod_const, card_fin]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ 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)))
have 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)))
Tactic: rw [sum_sigma']
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ 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)))
have 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)))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)))
⊢ 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)))
have h : ((Ico 2 (n + 1)).sigma (α := Composition) fun (k : ℕ) ↦ Set.toFinset {c : Composition k | 1 < c.length}) ⊆
  compPartialSumTarget 2 (n + 1) n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ 0 ≤
    r *
      (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
        p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j))
have positivity : 0 ≤ a →
  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)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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))
⊢ 0 ≤
    r *
      (a ^ x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j *
        p (x.snd (β := fun (i : ℕ) ↦ Composition i).blocksFun j))
have 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))
Tactic: positivity [ha, hp (x.snd.blocksFun j)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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)
⊢ Sigma.mk (β := fun (i : ℕ) ↦ Composition i) k c ∈ compPartialSumTarget 2 (n + 1) n
have hd₁ : (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
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ Sigma.mk (β := fun (i : ℕ) ↦ Composition i) k c ∈ compPartialSumTarget 2 (n + 1) n
have h : 2 ≤ c.length ∧ c.length < n + 1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n
Tactic: simp only [mem_compPartialSumTarget_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
have h : ∀ (j : Fin c.length), c.blocksFun j < n
Tactic: refine ⟨hd.2, c.length_le.trans_lt hd.1.2, fun j => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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.blocksFun j < n
have this : c ≠ Composition.single k sorry
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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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 ⋯
⊢ c.blocksFun j < n
have this₁ : ∀ (i : Fin c.length), c.blocksFun i < k
Tactic: rw [Composition.ne_single_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ 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)))
have 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)))
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ 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)))
have 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)))
Tactic: apply compChangeOfVariables_sum
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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
⊢ Eq (α := ℝ)
    (∏ j : Fin ⟨k, blocksFun⟩.fst,
      r *
        (HPow.hPow (β := ℕ) a
            (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j : ℕ) *
          p (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j)))
    (∏ j : Fin (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length,
      r *
        (a ^
            (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              j *
          p
            ((compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              j)))
have K : (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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ Eq (α := ℝ)
    (∏ j : Fin ⟨k, blocksFun⟩.fst,
      r *
        (HPow.hPow (β := ℕ) a
            (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j : ℕ) *
          p (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j)))
    (∏ j : Fin (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length,
      r *
        (a ^
            (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              j *
          p
            ((compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              j)))
have h : 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: congr 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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 :
  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
⊢ Eq (α := ℝ)
    (∏ j : Fin ⟨k, blocksFun⟩.fst,
      r *
        (HPow.hPow (β := ℕ) a
            (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j : ℕ) *
          p (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j)))
    (∏ j : Fin (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length,
      r *
        (a ^
            (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              j *
          p
            ((compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              j)))
have h₁ : 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: congr 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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 :
  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
h₁ :
  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
⊢ Eq (α := ℝ)
    (∏ j : Fin ⟨k, blocksFun⟩.fst,
      r *
        (HPow.hPow (β := ℕ) a
            (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j : ℕ) *
          p (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j)))
    (∏ j : Fin (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length,
      r *
        (a ^
            (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              j *
          p
            ((compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              j)))
have 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))) (β :=
  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: congr 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ 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
have h : Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) = k
Tactic: rw [K]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ 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
have h : Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) = k
Tactic: try rw [K]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ 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
have h : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun)) = Fin k
Tactic: rw [K]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ 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
have h : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun)) = Fin k
Tactic: try rw [K]