awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
h'c : c.length = 0
j : Fin c.length
hj : Membership.mem (γ := Finset (Fin c.length)) Finset.univ j
⊢ c.blocksFun j = 0
have this : (↑j : ℕ) < c.length
Tactic: have := j.2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
h'c : c.length = 0
⊢ ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n
have this : Eq (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) 0
Tactic: have : ∑ j : Fin c.length, c.blocksFun j = 0 := by
        apply Finset.sum_eq_zero (fun j hj ↦ ?_)
        have := j.2
        grind
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
h'c : c.length = 0
this : Eq (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) 0
⊢ ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n
have inl : 0 < m * n
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
h'c : 0 < c.length
⊢ LT.lt (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) (∑ j : Fin c.length, n)
have apply : ∃ (i_1 : Fin c.length), Membership.mem (γ := Finset (Fin c.length)) Finset.univ i_1 ∧ c.blocksFun i_1 < n
Tactic: apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
h'c : 0 < c.length
⊢ ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n
have calc : LT.lt (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) (∑ j : Fin c.length, n)
Tactic: calc ∑ j : Fin c.length, c.blocksFun j
      _ < ∑ j : Fin c.length, n := by
        apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)
        exact ⟨⟨0, h'c⟩, Finset.mem_univ _, hi _⟩
      _ = c.length * n := by simp
      _ ≤ m * n := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
h'c : 0 < c.length
calc : LT.lt (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) (∑ j : Fin c.length, n)
⊢ ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n
have calc₁ : ∑ j : Fin c.length, n = c.length * n
Tactic: calc ∑ j : Fin c.length, c.blocksFun j
      _ < ∑ j : Fin c.length, n := by
        apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)
        exact ⟨⟨0, h'c⟩, Finset.mem_univ _, hi _⟩
      _ = c.length * n := by simp
      _ ≤ m * n := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
h'c : 0 < c.length
calc : LT.lt (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) (∑ j : Fin c.length, n)
calc₁ : ∑ j : Fin c.length, n = c.length * n
⊢ ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n
have calc₂ : c.length * n ≤ m * n
Tactic: calc ∑ j : Fin c.length, c.blocksFun j
      _ < ∑ j : Fin c.length, n := by
        apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)
        exact ⟨⟨0, h'c⟩, Finset.mem_univ _, hi _⟩
      _ = c.length * n := by simp
      _ ≤ m * n := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
hi : m * n ≤ i
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
⊢ Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G) (0 : G)
have h : ∀ (j : Fin c.length) (hj : n ≤ c.blocksFun j),
  Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G) (0 : G)
Tactic: obtain ⟨j, hj⟩ : ∃ j, n ≤ c.blocksFun j := by
    contrapose! hi
    rw [← c.sum_blocksFun]
    rcases eq_zero_or_pos c.length with h'c | h'c
    · have : ∑ j : Fin c.length, c.blocksFun j = 0 := by
        apply Finset.sum_eq_zero (fun j hj ↦ ?_)
        have := j.2
        grind
      rw [this]
      exact mul_pos (by grind) hn
    · calc ∑ j : Fin c.length, c.blocksFun j
      _ < ∑ j : Fin c.length, n := by
        apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)
        exact ⟨⟨0, h'c⟩, Finset.mem_univ _, hi _⟩
      _ = c.length * n := by simp
      _ ≤ m * n := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
hi : m * n ≤ i
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
j : Fin c.length
hj : n ≤ c.blocksFun j
⊢ Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G) (0 : G)
have h : p.applyComposition c v j = 0
Tactic: apply ContinuousMultilinearMap.map_coord_zero _ j
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
hg : CPolynomialAt 𝕜 g (f x)
hf : CPolynomialAt 𝕜 f x
⊢ CPolynomialAt 𝕜 (g ∘ f) x
have rcases : ∀ (q : FormalMultilinearSeries 𝕜 F G) (m : ℕ) (hm : HasFiniteFPowerSeriesAt g q (f x) m), CPolynomialAt 𝕜 (g ∘ f) x
Tactic: rcases hg with ⟨q, m, hm⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
hf : CPolynomialAt 𝕜 f x
q : FormalMultilinearSeries 𝕜 F G
m : ℕ
hm : HasFiniteFPowerSeriesAt g q (f x) m
⊢ CPolynomialAt 𝕜 (g ∘ f) x
have rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (hn : HasFiniteFPowerSeriesAt f p x n), CPolynomialAt 𝕜 (g ∘ f) x
Tactic: rcases hf with ⟨p, n, hn⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
q : FormalMultilinearSeries 𝕜 F G
m : ℕ
hm : HasFiniteFPowerSeriesAt g q (f x) m
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : HasFiniteFPowerSeriesAt f p x n
⊢ CPolynomialAt 𝕜 (g ∘ f) x
have refine : HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * (n + 1))
Tactic: refine ⟨q.comp p, m * (n + 1), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
hg : CPolynomialAt 𝕜 g y
hf : CPolynomialAt 𝕜 f x
hy : f x = y
⊢ CPolynomialAt 𝕜 (g ∘ f) x
have hg₁ : CPolynomialAt 𝕜 g (f x)
Tactic: rw [← hy] at hg
Cleared hypotheses: hg, hf, hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
i j : (a : Composition n) × Composition a.length
⊢ i = j ↔
    i.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks =
        j.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks ∧
      i.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks =
        j.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks
have refine : i.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks =
      j.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks ∧
    i.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks =
      j.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks →
  i = j
Tactic: refine ⟨by rintro rfl; exact ⟨rfl, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
i j : (a : Composition n) × Composition a.length
⊢ i.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks =
        j.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks ∧
      i.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks =
        j.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks →
    i = j
have 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 =
        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 i with ⟨a, b⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
j : (a : Composition n) × Composition a.length
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 =
        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
have 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')
Tactic: rcases j with ⟨a', b'⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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 = a'
have blocks : a.blocks = a'.blocks
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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'))
⊢ 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')
have 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')
Tactic: obtain rfl : a = a' := by ext1; exact h
Cleared hypotheses: a', b', h, h'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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 = b'
have blocks : b.blocks = b'.blocks
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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'))
⊢ 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')
have 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)
Tactic: obtain rfl : b = b' := by ext1; exact h'
Cleared hypotheses: b', h, h'