awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
fst snd : ℕ
hn : 2 * max Nf Ng ≤ fst + snd
hi :
  (@Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)).Nonempty →
    (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
this : max Nf Ng ≤ snd
⊢ a * (ε / max a b) ≤ ε
have rw : a / max a b ≤ 1
Tactic: rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
fst snd : ℕ
hn : 2 * max Nf Ng ≤ fst + snd
hi :
  (@Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)).Nonempty →
    (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
this : max Nf Ng ≤ snd
⊢ norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) <
    ε
have calc : norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst *
    (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) <
  a * (ε / max a b)
Tactic: calc _ < a * (ε / max a b) := by
          grw [fBound1 fst]
          gcongr
          exact gBound2 snd (by omega)
         _ ≤ ε := by
          rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›]
          bound
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
inst_1 : IsUltrametricDist R
f g : R⟦X⟧
a : ℝ
ha : 1 ≤ a
b : ℝ
hb : 1 ≤ b
fBound1 : ∀ (a_1 : ℕ), norm (E := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ a_1 ≤ a
gBound1 : ∀ (a : ℕ), norm (E := R) ((coeff a : (a : R⟦X⟧) → R) g : R) * |c| ^ a ≤ b
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
Nf : ℕ
fBound2 : ∀ (n : ℕ), Nf ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / max a b
Ng : ℕ
gBound2 : ∀ (n : ℕ), Ng ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / max a b
fst snd : ℕ
hn : 2 * max Nf Ng ≤ fst + snd
hi :
  (@Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)).Nonempty →
    (fst, snd) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd)
ultrametric :
  norm.{u_1} (E := R)
      (∑ j ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (fst + snd),
        HMul.hMul (α := R) (β := R) ((coeff j.1 : (a : R⟦X⟧) → R) f : R) ((coeff j.2 : (a : R⟦X⟧) → R) g : R)) ≤
    ‖HMul.hMul (α := R) (β := R) ((coeff (fst, snd).1 : (a : R⟦X⟧) → R) f : R)
        ((coeff (fst, snd).2 : (a : R⟦X⟧) → R) g : R)‖
this : max Nf Ng ≤ snd
calc :
  norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) <
    a * (ε / max a b)
⊢ norm (E := R) ((coeff fst : (a : R⟦X⟧) → R) f : R) * |c| ^ fst *
      (norm (E := R) ((coeff snd : (a : R⟦X⟧) → R) g : R) * |c| ^ snd) <
    ε
have calc₁ : a * (ε / max a b) ≤ ε
Tactic: calc _ < a * (ε / max a b) := by
          grw [fBound1 fst]
          gcongr
          exact gBound2 snd (by omega)
         _ ≤ ε := by
          rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›]
          bound
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ (coeff n : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) = (n - 1).largeSchroder
have simp : ∑ k ∈ range (n + 1), HMul.hMul (α := ℕ) ((coeff k : (a : ℕ⟦X⟧) → ℕ) X : ℕ) (n - k).largeSchroder = (n - 1).largeSchroder
Tactic: simp only [coeff_mul, coeff_largeSchroderSeries,
    Nat.sum_antidiagonal_eq_sum_range_succ (coeff · X * largeSchroder ·),
    succ_eq_add_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ ∑ k ∈ range (n + 1), HMul.hMul (α := ℕ) ((coeff k : (a : ℕ⟦X⟧) → ℕ) X : ℕ) (n - k).largeSchroder =
    (n - 1).largeSchroder
have simp : n = 0 → 0 = (n - 1).largeSchroder
Tactic: simp only [coeff_X, ite_mul, one_mul, zero_mul, sum_ite_eq', mem_range, lt_add_iff_pos_left,
    ite_eq_left_iff, not_lt, nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
    (∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder : ℕ)
have rw : Eq (α := ℕ)
  (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
    HMul.hMul (α := ℕ) (β := ℕ) ((coeff p.1 : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
      ((coeff p.2 : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ))
  (∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder)
Tactic: rw [pow_two, ← mul_assoc, coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ Eq (α := ℕ)
    (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := ℕ) (β := ℕ) ((coeff p.1 : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
        ((coeff p.2 : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ))
    (∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder)
have rw : ∑ x ∈ range n,
      HMul.hMul (α := ℕ) (β := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
        ((coeff (n - x) : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ) +
    HMul.hMul (α := ℕ) (β := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
      ((coeff (n - n) : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ) =
  ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Tactic: rw [Nat.sum_antidiagonal_eq_sum_range_succ
    (fun x y => (coeff x) (X * largeSchroderSeries) * (coeff y) largeSchroderSeries) n,
    Nat.succ_eq_add_one, sum_range_succ]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ ∑ x ∈ range n,
        HMul.hMul (α := ℕ) (β := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
          ((coeff (n - x) : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ) +
      HMul.hMul (α := ℕ) (β := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
        ((coeff (n - n) : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ) =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
have simp : ∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder +
    (n - 1).largeSchroder =
  ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Tactic: simp only [coeff_largeSchroderSeries, coeff_X_mul_largeSchroderSeries n hn, tsub_self,
    largeSchroder_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
have apply : ∀ x ∈ range n,
  HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
    if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (hypothesis)
Goal:
n : ℕ
hn : 0 < n
x : ℕ
a : x ∈ range n
⊢ HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
    if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
have a₁ : x < n
Tactic: simp_all only [mem_range]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
x : ℕ
a : x < n
⊢ HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
    if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
have isTrue : 0 < x →
  HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
    (x - 1).largeSchroder * (n - x).largeSchroder
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
x : ℕ
a : x < n
isTrue :
  0 < x →
    HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
      (x - 1).largeSchroder * (n - x).largeSchroder
⊢ HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
    if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
have isFalse : ¬0 < x → HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder = 0
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h : 0 < x
⊢ HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder =
    (x - 1).largeSchroder * (n - x).largeSchroder
have simp_all : (coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) = (x - 1).largeSchroder ∨ (n - x).largeSchroder = 0
Tactic: simp_all only [mul_eq_mul_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (hypothesis)
Goal:
n : ℕ
hn : 0 < n
⊢ ∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder +
      (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
have this : Eq (α := ℕ)
  (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
  (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
Tactic: have : ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * largeSchroder (n - x) =
      ∑ x ∈ range n, if 0 < x then largeSchroder (x - 1) * largeSchroder (n - x) else 0 := by
    apply sum_congr rfl
    intro x a
    simp_all only [mem_range]
    split
    next h =>
      simp_all only [mul_eq_mul_right_iff]
      simp [coeff_X_mul_largeSchroderSeries x (by lia)]
    next h =>
      simp_all only [not_lt, nonpos_iff_eq_zero, coeff_zero_eq_constantCoeff, map_mul,
      constantCoeff_X, constantCoeff_largeSchroderSeries, mul_one, tsub_zero, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
⊢ ∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder +
      (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
have rw : ((if LT.lt (α := ℕ) 0 0 then (HSub.hSub (α := ℕ) 0 1).largeSchroder * (n - 0).largeSchroder else 0) +
      ∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) +
    (n - 1).largeSchroder =
  ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Tactic: rw [this, sum_range_eq_add_Ico _ (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
⊢ ((if LT.lt (α := ℕ) 0 0 then (HSub.hSub (α := ℕ) 0 1).largeSchroder * (n - 0).largeSchroder else 0) +
        ∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) +
      (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
have simp : (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) + (n - 1).largeSchroder =
  ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Tactic: simp only [lt_self_iff_false, reduceIte, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
⊢ Eq (α := ℕ) (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
    (∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder)
have apply : ∀ x ∈ Ico 1 n,
  (if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) = (x - 1).largeSchroder * (n - x).largeSchroder
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (hypothesis)
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
x : ℕ
hx : x ∈ Ico 1 n
⊢ (if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) = (x - 1).largeSchroder * (n - x).largeSchroder
have hx' : 0 < x
Tactic: have hx' : 0 < x := by grind
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
x : ℕ
hx : x ∈ Ico 1 n
hx' : 0 < x
⊢ (if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) = (x - 1).largeSchroder * (n - x).largeSchroder
have rw : (x - 1).largeSchroder * (n - x).largeSchroder = (x - 1).largeSchroder * (n - x).largeSchroder
Tactic: rw [if_pos hx']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (hypothesis)
Goal:
n : ℕ
hn : 0 < n
this :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
⊢ (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) + (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
have this₁ : Eq (α := ℕ) (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
  (∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder)
Tactic: have : (∑ x ∈ Ico 1 n, if 0 < x then largeSchroder (x - 1) * largeSchroder (n - x) else 0) =
    ∑ x ∈ Ico 1 n, largeSchroder (x - 1) * largeSchroder (n - x) := by
    apply sum_congr rfl
    intros x hx
    have hx' : 0 < x := by grind
    rw [if_pos hx']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : 0 < n
this_1 :
  Eq (α := ℕ)
    (∑ x ∈ range n, HMul.hMul (α := ℕ) ((coeff x : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ) (n - x).largeSchroder)
    (∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
this :
  Eq (α := ℕ) (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0)
    (∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder)
⊢ (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) + (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
have rw : ∑ k ∈ range (n - 1 + 1 - 1), (1 + k - 1).largeSchroder * (n - 1 + 1 - (1 + k)).largeSchroder +
    (n - 1 + 1 - 1).largeSchroder =
  ∑ x ∈ range (n - 1), x.largeSchroder * (n - 1 + 1 - 1 - x).largeSchroder +
    (n - 1).largeSchroder * (n - 1 + 1 - 1 - (n - 1)).largeSchroder
Tactic: rw [this, sum_Ico_eq_sum_range, show n = n - 1 + 1 by lia,
    sum_range_succ]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
⊢ largeSchroderSeries = 1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2
have h : ∀ (n : ℕ),
  Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
have pos : ∀ (hn : n = 0),
  Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
pos :
  ∀ (hn : n = 0),
    Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
      ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
have neg : ∀ (hn : ¬n = 0),
  Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (hypothesis)
Goal:
n : ℕ
hn : ¬n = 0
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
have hn' : 0 < n
Tactic: have hn' : 0 < n := by omega
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) largeSchroderSeries : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) (1 + X * largeSchroderSeries + X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
have neg : n.largeSchroder =
  HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
Tactic: simp only [coeff_largeSchroderSeries, map_add, coeff_one, hn, ↓reduceIte, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ n.largeSchroder =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * largeSchroderSeries) : ℕ)
      ((coeff n : (a : ℕ⟦X⟧) → ℕ) (X * HPow.hPow (β := ℕ) largeSchroderSeries 2) : ℕ)
have neg : (n - 1).largeSchroder + ∑ i ∈ Iic (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder =
  (n - 1 + 1 - 1).largeSchroder + ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 + 1 - 1 - i).largeSchroder
Tactic: rw [coeff_X_mul_largeSchroderSeriesSeries_sq _ hn', coeff_X_mul_largeSchroderSeries _ hn',
      show n = n - 1 + 1 by omega, largeSchroder_succ (n - 1)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ (n - 1).largeSchroder + ∑ i ∈ Iic (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder =
    (n - 1 + 1 - 1).largeSchroder + ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 + 1 - 1 - i).largeSchroder
have neg : Eq (α := ℕ) (∑ i ∈ Iic (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
  (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
Tactic: simp only [add_tsub_cancel_right, Nat.add_left_cancel_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ Eq (α := ℕ) (∑ i ∈ Iic (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
    (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
have neg : Eq (α := ℕ) (∑ i ∈ Icc ⊥ (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
  (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
Tactic: rw [Iic_eq_Icc, Nat.bot_eq_zero, ← range_succ_eq_Icc_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : ¬n = 0
hn' : 0 < n
neg :
  Eq (α := ℕ) (∑ i ∈ Icc ⊥ (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
    (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
⊢ Eq (α := ℕ) (∑ i ∈ Iic (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
    (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
have neg₁ : Eq (α := ℕ) (∑ i ∈ Icc 0 (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
  (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
Tactic: rw [Iic_eq_Icc, Nat.bot_eq_zero, ← range_succ_eq_Icc_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Schroder (goal)
Goal:
n : ℕ
hn : ¬n = 0
hn' : 0 < n
neg :
  Eq (α := ℕ) (∑ i ∈ Icc ⊥ (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
    (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
neg₁ :
  Eq (α := ℕ) (∑ i ∈ Icc 0 (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
    (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
⊢ Eq (α := ℕ) (∑ i ∈ Iic (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder)
    (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
have neg₂ : Eq (α := ℕ) (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
  (∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder)
Tactic: rw [Iic_eq_Icc, Nat.bot_eq_zero, ← range_succ_eq_Icc_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : DiscreteTopology S
a : MvPowerSeries τ S
⊢ HasSubst a ↔ HasEval a
have rw : MvPowerSeries.HasSubst (Function.const Unit a) ↔ HasEval a
Tactic: rw [hasSubst_iff, MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, hasEval_iff,
    Function.const_def]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : DiscreteTopology S
a : MvPowerSeries τ S
rw : MvPowerSeries.HasSubst (Function.const Unit a) ↔ HasEval a
⊢ HasSubst a ↔ HasEval a
have rw₁ : MvPowerSeries.HasEval (Function.const Unit a) ↔ HasEval a
Tactic: rw [hasSubst_iff, MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, hasEval_iff,
    Function.const_def]